:: SEMI_AF1 semantic presentation

definition

let IT be non empty AffinStruct ;
attr IT is Semi_Affine_Space-like means :Def1: :: SEMI_AF1:def 1
( ( for a, b being Element of IT holds a,b // b,a ) & ( for a, b, c being Element of IT holds a,b // c,c ) & ( for a, b, p, q, r, s being Element of IT st a <> b & a,b // p,q & a,b // r,s holds
p,q // r,s ) & ( for a, b, c being Element of IT st a,b // a,c holds
b,a // b,c ) & not for a, b, c being Element of IT holds a,b // a,c & ( for a, b, p being Element of IT ex q being Element of IT st
( a,b // p,q & a,p // b,q ) ) & ( for o, a being Element of IT ex p being Element of IT st
for b, c being Element of IT holds
( o,a // o,p & ex d being Element of IT st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) ) & ( for o, a, a', b, b', c, c' being Element of IT st not o,a // o,b & not o,a // o,c & o,a // o,a' & o,b // o,b' & o,c // o,c' & a,b // a',b' & a,c // a',c' holds
b,c // b',c' ) & ( for a, a', b, b', c, c' being Element of IT st not a,a' // a,b & not a,a' // a,c & a,a' // b,b' & a,a' // c,c' & a,b // a',b' & a,c // a',c' holds
b,c // b',c' ) & ( for a1, a2, a3, b1, b2, b3 being Element of IT st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds
a3,b1 // a1,b3 ) & ( for a, b, c, d being Element of IT st not a,b // a,c & a,b // c,d & a,c // b,d holds
not a,d // b,c ) );

end;

:: deftheorem Def1 defines Semi_Affine_Space-like SEMI_AF1:def 1 :

registration

cluster non empty Semi_Affine_Space-like AffinStruct ;
existence

proof end;

end;

definition

mode Semi_Affine_Space is non empty Semi_Affine_Space-like AffinStruct ;

end;

theorem :: SEMI_AF1:1

canceled;

theorem :: SEMI_AF1:2

canceled;

theorem :: SEMI_AF1:3

canceled;

theorem :: SEMI_AF1:4

canceled;

theorem :: SEMI_AF1:5

canceled;

theorem :: SEMI_AF1:6

canceled;

theorem :: SEMI_AF1:7

canceled;

theorem :: SEMI_AF1:8

canceled;

theorem :: SEMI_AF1:9

canceled;

theorem :: SEMI_AF1:10

canceled;

theorem :: SEMI_AF1:11

canceled;

theorem Th12: :: SEMI_AF1:12

for SAS being Semi_Affine_Space
for a, b being Element of SAS holds a,b // a,b

proof end;

theorem Th13: :: SEMI_AF1:13

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st a,b // c,d holds
c,d // a,b

proof end;

theorem Th14: :: SEMI_AF1:14

for SAS being Semi_Affine_Space
for a, b, c being Element of SAS holds a,a // b,c

proof end;

theorem Th15: :: SEMI_AF1:15

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st a,b // c,d holds
b,a // c,d

proof end;

theorem Th16: :: SEMI_AF1:16

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st a,b // c,d holds
a,b // d,c

proof end;

theorem Th17: :: SEMI_AF1:17

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st a,b // c,d holds
( b,a // c,d & a,b // d,c & b,a // d,c & c,d // a,b & d,c // a,b & c,d // b,a & d,c // b,a )

proof end;

theorem Th18: :: SEMI_AF1:18

for SAS being Semi_Affine_Space
for a, b, c being Element of SAS st a,b // a,c holds
( a,c // a,b & b,a // a,c & a,b // c,a & a,c // b,a & b,a // c,a & c,a // a,b & c,a // b,a & b,a // b,c & a,b // b,c & b,a // c,b & b,c // b,a & a,b // c,b & c,b // b,a & b,c // a,b & c,b // a,b & c,a // c,b & a,c // c,b & c,a // b,c & a,c // b,c & c,b // c,a & b,c // c,a & c,b // a,c & b,c // a,c )

proof end;

theorem :: SEMI_AF1:19

canceled;

theorem Th20: :: SEMI_AF1:20

for SAS being Semi_Affine_Space
for a, b, p, q, r, s being Element of SAS st a <> b & p,q // a,b & a,b // r,s holds
p,q // r,s

proof end;

theorem :: SEMI_AF1:21

for SAS being Semi_Affine_Space
for a, b, d being Element of SAS st not a,b // a,d holds
( a <> b & b <> d & d <> a ) by Def1, Th12, Th14;

theorem :: SEMI_AF1:22

for SAS being Semi_Affine_Space
for a, b, p, q being Element of SAS st not a,b // p,q holds
( a <> b & p <> q ) by Def1, Th14;

theorem :: SEMI_AF1:23

for SAS being Semi_Affine_Space
for a, b, x, c being Element of SAS st a,b // a,x & b,c // b,x & c,a // c,x holds
a,b // a,c

proof end;

theorem :: SEMI_AF1:24

canceled;

theorem Th25: :: SEMI_AF1:25

for SAS being Semi_Affine_Space
for a, b, c, p, q being Element of SAS st not a,b // a,c & p <> q & p,q // p,a & p,q // p,b holds
not p,q // p,c

proof end;

theorem Th26: :: SEMI_AF1:26

for SAS being Semi_Affine_Space
for p, q being Element of SAS st p <> q holds
ex r being Element of SAS st not p,q // p,r

proof end;

theorem :: SEMI_AF1:27

canceled;

theorem Th28: :: SEMI_AF1:28

for SAS being Semi_Affine_Space
for a, b, c being Element of SAS st not a,b // a,c holds
( not a,b // c,a & not b,a // a,c & not b,a // c,a & not a,c // a,b & not a,c // b,a & not c,a // a,b & not c,a // b,a & not b,a // b,c & not b,a // c,b & not a,b // b,c & not a,b // c,b & not b,c // b,a & not b,c // a,b & not c,b // a,b & not c,b // b,a & not c,b // c,a & not c,b // a,c & not b,c // c,a & not b,c // a,c & not c,a // c,b & not c,a // b,c & not a,c // b,c & not a,c // c,b )

proof end;

theorem Th29: :: SEMI_AF1:29

for SAS being Semi_Affine_Space
for a, b, c, d, p, q, r, s being Element of SAS st not a,b // c,d & a,b // p,q & c,d // r,s & p <> q & r <> s holds
not p,q // r,s

proof end;

theorem Th30: :: SEMI_AF1:30

for SAS being Semi_Affine_Space
for a, b, c, p, q, r being Element of SAS st not a,b // a,c & a,b // p,q & a,c // p,r & b,c // q,r & p <> q holds
not p,q // p,r

proof end;

theorem Th31: :: SEMI_AF1:31

for SAS being Semi_Affine_Space
for a, b, c, p, r being Element of SAS st not a,b // a,c & a,c // p,r & b,c // p,r holds
p = r

proof end;

theorem Th32: :: SEMI_AF1:32

for SAS being Semi_Affine_Space
for p, q, r1, r2 being Element of SAS st not p,q // p,r1 & p,r1 // p,r2 & q,r1 // q,r2 holds
r1 = r2

proof end;

theorem Th33: :: SEMI_AF1:33

for SAS being Semi_Affine_Space
for a, b, c, p, q, r1, r2 being Element of SAS st not a,b // a,c & a,b // p,q & a,c // p,r1 & a,c // p,r2 & b,c // q,r1 & b,c // q,r2 holds
r1 = r2

proof end;

theorem :: SEMI_AF1:34

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st ( a = b or c = d or ( a = c & b = d ) or ( a = d & b = c ) ) holds
a,b // c,d by Def1, Th12, Th14;

theorem :: SEMI_AF1:35

for SAS being Semi_Affine_Space
for a, b, c being Element of SAS st ( a = b or a = c or b = c ) holds
a,b // a,c by Def1, Th12, Th14;

definition

let SAS be Semi_Affine_Space;
let a, b, c be Element of SAS;
pred a,b,c is_collinear means :Def2: :: SEMI_AF1:def 2
a,b // a,c;

end;

:: deftheorem Def2 defines is_collinear SEMI_AF1:def 2 :

theorem :: SEMI_AF1:36

canceled;

theorem Th37: :: SEMI_AF1:37

for SAS being Semi_Affine_Space
for a1, a2, a3 being Element of SAS st a1,a2,a3 is_collinear holds
( a1,a3,a2 is_collinear & a2,a1,a3 is_collinear & a2,a3,a1 is_collinear & a3,a1,a2 is_collinear & a3,a2,a1 is_collinear )

proof end;

theorem :: SEMI_AF1:38

canceled;

theorem Th39: :: SEMI_AF1:39

for SAS being Semi_Affine_Space
for a, b, c, p, q, r being Element of SAS st not a,b,c is_collinear & a,b // p,q & a,c // p,r & p <> q & p <> r holds
not p,q,r is_collinear

proof end;

theorem Th40: :: SEMI_AF1:40

for SAS being Semi_Affine_Space
for a, b, c being Element of SAS st ( a = b or b = c or c = a ) holds
a,b,c is_collinear

proof end;

theorem Th41: :: SEMI_AF1:41

for SAS being Semi_Affine_Space
for p, q being Element of SAS st p <> q holds
ex r being Element of SAS st not p,q,r is_collinear

proof end;

theorem Th42: :: SEMI_AF1:42

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st a,b,c is_collinear & a,b,d is_collinear holds
a,b // c,d

proof end;

theorem Th43: :: SEMI_AF1:43

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st not a,b,c is_collinear & a,b // c,d holds
not a,b,d is_collinear

proof end;

theorem Th44: :: SEMI_AF1:44

for SAS being Semi_Affine_Space
for a, b, c, d, x being Element of SAS st not a,b,c is_collinear & a,b // c,d & c <> d & c,d,x is_collinear holds
not a,b,x is_collinear

proof end;

theorem :: SEMI_AF1:45

for SAS being Semi_Affine_Space
for o, a, b, x being Element of SAS st not o,a,b is_collinear & o,a,x is_collinear & o,b,x is_collinear holds
o = x

proof end;

theorem :: SEMI_AF1:46

for SAS being Semi_Affine_Space
for o, a, b, a', b' being Element of SAS st o <> a & o <> b & o,a,b is_collinear & o,a,a' is_collinear & o,b,b' is_collinear holds
a,b // a',b'

proof end;

theorem :: SEMI_AF1:47

canceled;

theorem :: SEMI_AF1:48

for SAS being Semi_Affine_Space
for a, b, c, d, p1, p2 being Element of SAS st not a,b // c,d & a,b,p1 is_collinear & a,b,p2 is_collinear & c,d,p1 is_collinear & c,d,p2 is_collinear holds
p1 = p2

proof end;

theorem Th49: :: SEMI_AF1:49

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st a <> b & a,b,c is_collinear & a,b // c,d holds
a,c // b,d

proof end;

theorem Th50: :: SEMI_AF1:50

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st a <> b & a,b,c is_collinear & a,b // c,d holds
c,b // c,d

proof end;

theorem Th51: :: SEMI_AF1:51

for SAS being Semi_Affine_Space
for o, a, c, b, d1, d2 being Element of SAS st not o,a,c is_collinear & o,a,b is_collinear & o,c,d1 is_collinear & o,c,d2 is_collinear & a,c // b,d1 & a,c // b,d1 & a,c // b,d2 holds
d1 = d2

proof end;

theorem :: SEMI_AF1:52

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st a <> b & a,b,c is_collinear & a,b,d is_collinear holds
a,c,d is_collinear

proof end;

definition

let SAS be Semi_Affine_Space;
let a, b, c, d be Element of SAS;
pred parallelogram a,b,c,d means :Def3: :: SEMI_AF1:def 3
( not a,b,c is_collinear & a,b // c,d & a,c // b,d );

end;

:: deftheorem Def3 defines parallelogram SEMI_AF1:def 3 :

theorem :: SEMI_AF1:53

canceled;

theorem Th54: :: SEMI_AF1:54

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds
( a <> b & a <> c & c <> b & a <> d & b <> d & c <> d )

proof end;

theorem Th55: :: SEMI_AF1:55

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds
( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear )

proof end;

theorem Th56: :: SEMI_AF1:56

for SAS being Semi_Affine_Space
for a1, a2, a3, a4 being Element of SAS st parallelogram a1,a2,a3,a4 holds
( not a1,a2,a3 is_collinear & not a1,a3,a2 is_collinear & not a1,a2,a4 is_collinear & not a1,a4,a2 is_collinear & not a1,a3,a4 is_collinear & not a1,a4,a3 is_collinear & not a2,a1,a3 is_collinear & not a2,a3,a1 is_collinear & not a2,a1,a4 is_collinear & not a2,a4,a1 is_collinear & not a2,a3,a4 is_collinear & not a2,a4,a3 is_collinear & not a3,a1,a2 is_collinear & not a3,a2,a1 is_collinear & not a3,a1,a4 is_collinear & not a3,a4,a1 is_collinear & not a3,a2,a4 is_collinear & not a3,a4,a2 is_collinear & not a4,a1,a2 is_collinear & not a4,a2,a1 is_collinear & not a4,a1,a3 is_collinear & not a4,a3,a1 is_collinear & not a4,a2,a3 is_collinear & not a4,a3,a2 is_collinear )

proof end;

theorem Th57: :: SEMI_AF1:57

for SAS being Semi_Affine_Space
for a, b, c, d, x being Element of SAS holds
( not parallelogram a,b,c,d or not a,b,x is_collinear or not c,d,x is_collinear )

proof end;

theorem :: SEMI_AF1:58

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds
parallelogram a,c,b,d

proof end;

theorem :: SEMI_AF1:59

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds
parallelogram c,d,a,b

proof end;

theorem :: SEMI_AF1:60

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds
parallelogram b,a,d,c

proof end;

theorem Th61: :: SEMI_AF1:61

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds
( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c )

proof end;

theorem Th62: :: SEMI_AF1:62

for SAS being Semi_Affine_Space
for a, b, c being Element of SAS st not a,b,c is_collinear holds
ex d being Element of SAS st parallelogram a,b,c,d

proof end;

theorem Th63: :: SEMI_AF1:63

for SAS being Semi_Affine_Space
for a, b, c, d1, d2 being Element of SAS st parallelogram a,b,c,d1 & parallelogram a,b,c,d2 holds
d1 = d2

proof end;

theorem Th64: :: SEMI_AF1:64

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds
not a,d // b,c

proof end;

theorem Th65: :: SEMI_AF1:65

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds
not parallelogram a,b,d,c

proof end;

theorem Th66: :: SEMI_AF1:66

for SAS being Semi_Affine_Space
for a, b being Element of SAS st a <> b holds
ex c being Element of SAS st
( a,b,c is_collinear & c <> a & c <> b )

proof end;

theorem Th67: :: SEMI_AF1:67

for SAS being Semi_Affine_Space
for a, a', b, b', c, c' being Element of SAS st parallelogram a,a',b,b' & parallelogram a,a',c,c' holds
b,c // b',c'

proof end;

theorem Th68: :: SEMI_AF1:68

for SAS being Semi_Affine_Space
for b, b', c, a, a', c' being Element of SAS st not b,b',c is_collinear & parallelogram a,a',b,b' & parallelogram a,a',c,c' holds
parallelogram b,b',c,c'

proof end;

theorem Th69: :: SEMI_AF1:69

for SAS being Semi_Affine_Space
for a, b, c, a', b', c' being Element of SAS st a,b,c is_collinear & b <> c & parallelogram a,a',b,b' & parallelogram a,a',c,c' holds
parallelogram b,b',c,c'

proof end;

theorem Th70: :: SEMI_AF1:70

for SAS being Semi_Affine_Space
for a, a', b, b', c, c', d, d' being Element of SAS st parallelogram a,a',b,b' & parallelogram a,a',c,c' & parallelogram b,b',d,d' holds
c,d // c',d'

proof end;

Lm1: for SAS being Semi_Affine_Space
for a, b being Element of SAS st a <> b holds
ex c, d being Element of SAS st parallelogram a,b,c,d

proof end;

theorem :: SEMI_AF1:71

for SAS being Semi_Affine_Space
for a, d being Element of SAS st a <> d holds
ex b, c being Element of SAS st parallelogram a,b,c,d

proof end;

definition

let SAS be Semi_Affine_Space;
let a, b, r, s be Element of SAS;
pred congr a,b,r,s means :Def4: :: SEMI_AF1:def 4
( ( a = b & r = s ) or ex p, q being Element of SAS st
( parallelogram p,q,a,b & parallelogram p,q,r,s ) );

end;

:: deftheorem Def4 defines congr SEMI_AF1:def 4 :

theorem :: SEMI_AF1:72

canceled;

theorem Th73: :: SEMI_AF1:73

for SAS being Semi_Affine_Space
for a, b, c being Element of SAS st congr a,a,b,c holds
b = c

proof end;

theorem Th74: :: SEMI_AF1:74

for SAS being Semi_Affine_Space
for a, b, c being Element of SAS st congr a,b,c,c holds
a = b

proof end;

theorem Th75: :: SEMI_AF1:75

for SAS being Semi_Affine_Space
for a, b being Element of SAS st congr a,b,b,a holds
a = b

proof end;

theorem Th76: :: SEMI_AF1:76

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st congr a,b,c,d holds
a,b // c,d

proof end;

theorem Th77: :: SEMI_AF1:77

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st congr a,b,c,d holds
a,c // b,d

proof end;

theorem Th78: :: SEMI_AF1:78

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st congr a,b,c,d & not a,b,c is_collinear holds
parallelogram a,b,c,d

proof end;

theorem Th79: :: SEMI_AF1:79

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds
congr a,b,c,d

proof end;

theorem Th80: :: SEMI_AF1:80

for SAS being Semi_Affine_Space
for a, b, c, d, r, s being Element of SAS st congr a,b,c,d & a,b,c is_collinear & parallelogram r,s,a,b holds
parallelogram r,s,c,d

proof end;

theorem Th81: :: SEMI_AF1:81

for SAS being Semi_Affine_Space
for a, b, c, x, y being Element of SAS st congr a,b,c,x & congr a,b,c,y holds
x = y

proof end;

theorem Th82: :: SEMI_AF1:82

for SAS being Semi_Affine_Space
for a, b, c being Element of SAS ex d being Element of SAS st congr a,b,c,d

proof end;

theorem :: SEMI_AF1:83

canceled;

theorem Th84: :: SEMI_AF1:84

for SAS being Semi_Affine_Space
for a, b being Element of SAS holds congr a,b,a,b

proof end;

theorem Th85: :: SEMI_AF1:85

for SAS being Semi_Affine_Space
for r, s, a, b, c, d being Element of SAS st congr r,s,a,b & congr r,s,c,d holds
congr a,b,c,d

proof end;

theorem Th86: :: SEMI_AF1:86

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st congr a,b,c,d holds
congr c,d,a,b

proof end;

theorem Th87: :: SEMI_AF1:87

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st congr a,b,c,d holds
congr b,a,d,c

proof end;

theorem Th88: :: SEMI_AF1:88

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st congr a,b,c,d holds
congr a,c,b,d

proof end;

theorem Th89: :: SEMI_AF1:89

for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st congr a,b,c,d holds
( congr c,d,a,b & congr b,a,d,c & congr a,c,b,d & congr d,c,b,a & congr b,d,a,c & congr c,a,d,b & congr d,b,c,a )

proof end;

theorem Th90: :: SEMI_AF1:90

for SAS being Semi_Affine_Space
for a, b, p, q, c, s being Element of SAS st congr a,b,p,q & congr b,c,q,s holds
congr a,c,p,s

proof end;

theorem Th91: :: SEMI_AF1:91

for SAS being Semi_Affine_Space
for b, a, p, q, c, r being Element of SAS st congr b,a,p,q & congr c,a,p,r holds
congr b,c,r,q

proof end;

theorem :: SEMI_AF1:92

for SAS being Semi_Affine_Space
for a, o, p, b, q being Element of SAS st congr a,o,o,p & congr b,o,o,q holds
congr a,b,q,p by Th91;

theorem Th93: :: SEMI_AF1:93

for SAS being Semi_Affine_Space
for b, a, p, q, c, r being Element of SAS st congr b,a,p,q & congr c,a,p,r holds
b,c // q,r

proof end;

theorem :: SEMI_AF1:94

for SAS being Semi_Affine_Space
for a, o, p, b, q being Element of SAS st congr a,o,o,p & congr b,o,o,q holds
a,b // p,q by Th93;

definition

let SAS be Semi_Affine_Space;
let a, b, o be Element of SAS;
func sum a,b,o -> Element of SAS means :Def5: :: SEMI_AF1:def 5
congr o,a,b,it;
correctness by Th81, Th82;

end;

:: deftheorem Def5 defines sum SEMI_AF1:def 5 :

definition

let SAS be Semi_Affine_Space;
let a, o be Element of SAS;
func opposite a,o -> Element of SAS means :Def6: :: SEMI_AF1:def 6
sum a,it,o = o;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines opposite SEMI_AF1:def 6 :

definition

let SAS be Semi_Affine_Space;
let a, b, o be Element of SAS;
func diff a,b,o -> Element of SAS equals :: SEMI_AF1:def 7
sum a,(opposite b,o),o;
correctness ;

end;

:: deftheorem defines diff SEMI_AF1:def 7 :

theorem :: SEMI_AF1:95

canceled;

theorem :: SEMI_AF1:96

canceled;

theorem :: SEMI_AF1:97

canceled;

theorem :: SEMI_AF1:98

canceled;

theorem Th99: :: SEMI_AF1:99

for SAS being Semi_Affine_Space
for a, o being Element of SAS holds sum a,o,o = a

proof end;

theorem :: SEMI_AF1:100

for SAS being Semi_Affine_Space
for a, o being Element of SAS ex x being Element of SAS st sum a,x,o = o

proof end;

theorem :: SEMI_AF1:101

for SAS being Semi_Affine_Space
for a, b, o, c being Element of SAS holds sum (sum a,b,o),c,o = sum a,(sum b,c,o),o

proof end;

theorem Th102: :: SEMI_AF1:102

for SAS being Semi_Affine_Space
for a, b, o being Element of SAS holds sum a,b,o = sum b,a,o

proof end;

theorem :: SEMI_AF1:103

for SAS being Semi_Affine_Space
for a, o being Element of SAS st sum a,a,o = o holds
a = o

proof end;

theorem Th104: :: SEMI_AF1:104

for SAS being Semi_Affine_Space
for a, x, o, y being Element of SAS st sum a,x,o = sum a,y,o holds
x = y

proof end;

theorem :: SEMI_AF1:105

canceled;

theorem Th106: :: SEMI_AF1:106

for SAS being Semi_Affine_Space
for a, o being Element of SAS holds congr a,o,o, opposite a,o

proof end;

theorem Th107: :: SEMI_AF1:107

for SAS being Semi_Affine_Space
for a, o, b being Element of SAS st opposite a,o = opposite b,o holds
a = b

proof end;

theorem :: SEMI_AF1:108

for SAS being Semi_Affine_Space
for a, b, o being Element of SAS holds a,b // opposite a,o, opposite b,o

proof end;

theorem :: SEMI_AF1:109

for SAS being Semi_Affine_Space
for o being Element of SAS holds opposite o,o = o

proof end;

theorem Th110: :: SEMI_AF1:110

for SAS being Semi_Affine_Space
for p, q, r, o being Element of SAS holds p,q // sum p,r,o, sum q,r,o

proof end;

theorem :: SEMI_AF1:111

for SAS being Semi_Affine_Space
for p, q, r, s, o being Element of SAS st p,q // r,s holds
p,q // sum p,r,o, sum q,s,o

proof end;

theorem :: SEMI_AF1:112

canceled;

theorem Th113: :: SEMI_AF1:113

for SAS being Semi_Affine_Space
for a, b, o being Element of SAS holds
( diff a,b,o = o iff a = b )

proof end;

theorem Th114: :: SEMI_AF1:114

for SAS being Semi_Affine_Space
for o, b, a being Element of SAS holds o, diff b,a,o // a,b

proof end;

theorem :: SEMI_AF1:115

for SAS being Semi_Affine_Space
for o, b, a, d, c being Element of SAS holds
( o, diff b,a,o, diff d,c,o is_collinear iff a,b // c,d )

proof end;

definition

let SAS be Semi_Affine_Space;
let a, b, c, d, o be Element of SAS;
pred trap a,b,c,d,o means :Def8: :: SEMI_AF1:def 8
( not o,a,c is_collinear & o,a,b is_collinear & o,c,d is_collinear & a,c // b,d );

end;

:: deftheorem Def8 defines trap SEMI_AF1:def 8 :

definition

let SAS be Semi_Affine_Space;
let o, p be Element of SAS;
pred qtrap o,p means :Def9: :: SEMI_AF1:def 9
for b, c being Element of SAS ex d being Element of SAS st
( o,p,b is_collinear implies ( o,c,d is_collinear & p,c // b,d ) );

end;

:: deftheorem Def9 defines qtrap SEMI_AF1:def 9 :

theorem :: SEMI_AF1:116

canceled;

theorem :: SEMI_AF1:117

canceled;

theorem Th118: :: SEMI_AF1:118

for SAS being Semi_Affine_Space
for a, b, c, d, o being Element of SAS st trap a,b,c,d,o holds
( o <> a & a <> c & c <> o )

proof end;

theorem :: SEMI_AF1:119

for SAS being Semi_Affine_Space
for a, b, c, x, o, y being Element of SAS st trap a,b,c,x,o & trap a,b,c,y,o holds
x = y

proof end;

theorem :: SEMI_AF1:120

for SAS being Semi_Affine_Space
for o, a, b being Element of SAS st not o,a,b is_collinear holds
trap a,o,b,o,o

proof end;

theorem Th121: :: SEMI_AF1:121

for SAS being Semi_Affine_Space
for a, b, c, d, o being Element of SAS st trap a,b,c,d,o holds
trap c,d,a,b,o

proof end;

theorem Th122: :: SEMI_AF1:122

for SAS being Semi_Affine_Space
for o, b, a, c, d being Element of SAS st o <> b & trap a,b,c,d,o holds
o <> d

proof end;

theorem Th123: :: SEMI_AF1:123

for SAS being Semi_Affine_Space
for o, b, a, c, d being Element of SAS st o <> b & trap a,b,c,d,o holds
not o,b,d is_collinear

proof end;

theorem :: SEMI_AF1:124

for SAS being Semi_Affine_Space
for o, b, a, c, d being Element of SAS st o <> b & trap a,b,c,d,o holds
trap b,a,d,c,o

proof end;

theorem Th125: :: SEMI_AF1:125

for SAS being Semi_Affine_Space
for o, b, d, a, c being Element of SAS st ( o = b or o = d ) & trap a,b,c,d,o holds
( o = b & o = d )

proof end;

theorem Th126: :: SEMI_AF1:126

for SAS being Semi_Affine_Space
for a, p, b, q, o, c, r being Element of SAS st trap a,p,b,q,o & trap a,p,c,r,o holds
b,c // q,r

proof end;

theorem Th127: :: SEMI_AF1:127

for SAS being Semi_Affine_Space
for a, p, b, q, o, c, r being Element of SAS st trap a,p,b,q,o & trap a,p,c,r,o & not o,b,c is_collinear holds
trap b,q,c,r,o

proof end;

theorem :: SEMI_AF1:128

for SAS being Semi_Affine_Space
for a, p, b, q, o, c, r, d, s being Element of SAS st trap a,p,b,q,o & trap a,p,c,r,o & trap b,q,d,s,o holds
c,d // r,s

proof end;

theorem Th129: :: SEMI_AF1:129

for SAS being Semi_Affine_Space
for o, a being Element of SAS ex p being Element of SAS st
( o,a,p is_collinear & qtrap o,p )

proof end;

theorem Th130: :: SEMI_AF1:130

for SAS being Semi_Affine_Space ex x, y, z being Element of SAS st
( x <> y & y <> z & z <> x )

proof end;

theorem Th131: :: SEMI_AF1:131

for SAS being Semi_Affine_Space
for o, p being Element of SAS st qtrap o,p holds
o <> p

proof end;

theorem :: SEMI_AF1:132

for SAS being Semi_Affine_Space
for o, p being Element of SAS st qtrap o,p holds
ex q being Element of SAS st
( not o,p,q is_collinear & qtrap o,q )

proof end;

theorem :: SEMI_AF1:133

for SAS being Semi_Affine_Space
for o, p, c, b being Element of SAS st not o,p,c is_collinear & o,p,b is_collinear & qtrap o,p holds
ex d being Element of SAS st trap p,b,c,d,o

proof end;