:: Semi-Affine Space
:: by Eugeniusz Kusak and Krzysztof Radziszewski
::
:: Received November 30, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let IT be non empty AffinStruct ;
attrIT is Semi_Affine_Space-like  means :Def1: :: SEMI_AF1:def 1
( ( for a, b being Element of IT holds a,b // b,a ) &amp; ( for a, b, c being Element of IT holds a,b // c,c ) &amp; ( for a, b, p, q, r, s being Element of IT st a <> b &amp; a,b // p,q &amp; a,b // r,s holds
p,q // r,s ) &amp; ( for a, b, c being Element of IT st a,b // a,c holds
b,a // b,c ) &amp; not for a, b, c being Element of IT holds a,b // a,c &amp; ( for a, b, p being Element of IT ex q being Element of IT st
( a,b // p,q &amp; a,p // b,q ) ) &amp; ( 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 &amp; ex d being Element of IT st
( o,p // o,b implies ( o,c // o,d &amp; p,c // b,d ) ) ) ) &amp; ( for o, a, a9, b, b9, c, c9 being Element of IT st not o,a // o,b &amp; not o,a // o,c &amp; o,a // o,a9 &amp; o,b // o,b9 &amp; o,c // o,c9 &amp; a,b // a9,b9 &amp; a,c // a9,c9 holds
b,c // b9,c9 ) &amp; ( for a, a9, b, b9, c, c9 being Element of IT st not a,a9 // a,b &amp; not a,a9 // a,c &amp; a,a9 // b,b9 &amp; a,a9 // c,c9 &amp; a,b // a9,b9 &amp; a,c // a9,c9 holds
b,c // b9,c9 ) &amp; ( for a1, a2, a3, b1, b2, b3 being Element of IT st a1,a2 // a1,a3 &amp; b1,b2 // b1,b3 &amp; a1,b2 // a2,b1 &amp; a2,b3 // a3,b2 holds
a3,b1 // a1,b3 ) &amp; ( for a, b, c, d being Element of IT st not a,b // a,c &amp; a,b // c,d &amp; a,c // b,d holds
not a,d // b,c ) );
end;

:: deftheorem Def1 defines Semi_Affine_Space-like SEMI_AF1:def_1_:_
 for IT being non empty AffinStruct holds
( IT is Semi_Affine_Space-like iff ( ( for a, b being Element of IT holds a,b // b,a ) &amp; ( for a, b, c being Element of IT holds a,b // c,c ) &amp; ( for a, b, p, q, r, s being Element of IT st a <> b &amp; a,b // p,q &amp; a,b // r,s holds
p,q // r,s ) &amp; ( for a, b, c being Element of IT st a,b // a,c holds
b,a // b,c ) &amp; not for a, b, c being Element of IT holds a,b // a,c &amp; ( for a, b, p being Element of IT ex q being Element of IT st
( a,b // p,q &amp; a,p // b,q ) ) &amp; ( 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 &amp; ex d being Element of IT st
( o,p // o,b implies ( o,c // o,d &amp; p,c // b,d ) ) ) ) &amp; ( for o, a, a9, b, b9, c, c9 being Element of IT st not o,a // o,b &amp; not o,a // o,c &amp; o,a // o,a9 &amp; o,b // o,b9 &amp; o,c // o,c9 &amp; a,b // a9,b9 &amp; a,c // a9,c9 holds
b,c // b9,c9 ) &amp; ( for a, a9, b, b9, c, c9 being Element of IT st not a,a9 // a,b &amp; not a,a9 // a,c &amp; a,a9 // b,b9 &amp; a,a9 // c,c9 &amp; a,b // a9,b9 &amp; a,c // a9,c9 holds
b,c // b9,c9 ) &amp; ( for a1, a2, a3, b1, b2, b3 being Element of IT st a1,a2 // a1,a3 &amp; b1,b2 // b1,b3 &amp; a1,b2 // a2,b1 &amp; a2,b3 // a3,b2 holds
a3,b1 // a1,b3 ) &amp; ( for a, b, c, d being Element of IT st not a,b // a,c &amp; a,b // c,d &amp; a,c // b,d holds
not a,d // b,c ) ) );

registration
cluster non empty Semi_Affine_Space-like for AffinStruct ;
existence
 ex b1 being non empty AffinStruct st b1 is Semi_Affine_Space-like
proofend;
end;

definition
mode Semi_Affine_Space is non empty Semi_Affine_Space-like AffinStruct ;
end;

theorem Th1: :: SEMI_AF1:1
for SAS being Semi_Affine_Space
for a, b being Element of SAS holds a,b // a,b
proofend;

theorem Th2: :: SEMI_AF1:2
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
proofend;

theorem Th3: :: SEMI_AF1:3
for SAS being Semi_Affine_Space
for a, b, c being Element of SAS holds a,a // b,c
proofend;

theorem Th4: :: SEMI_AF1:4
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
proofend;

theorem Th5: :: SEMI_AF1:5
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
proofend;

theorem Th6: :: SEMI_AF1:6
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 &amp; a,b // d,c &amp; b,a // d,c &amp; c,d // a,b &amp; d,c // a,b &amp; c,d // b,a &amp; d,c // b,a )
proofend;

theorem Th7: :: SEMI_AF1:7
for SAS being Semi_Affine_Space
for a, b, c being Element of SAS st a,b // a,c holds
( a,c // a,b &amp; b,a // a,c &amp; a,b // c,a &amp; a,c // b,a &amp; b,a // c,a &amp; c,a // a,b &amp; c,a // b,a &amp; b,a // b,c &amp; a,b // b,c &amp; b,a // c,b &amp; b,c // b,a &amp; a,b // c,b &amp; c,b // b,a &amp; b,c // a,b &amp; c,b // a,b &amp; c,a // c,b &amp; a,c // c,b &amp; c,a // b,c &amp; a,c // b,c &amp; c,b // c,a &amp; b,c // c,a &amp; c,b // a,c &amp; b,c // a,c )
proofend;

theorem Th8: :: SEMI_AF1:8
for SAS being Semi_Affine_Space
for a, b, p, q, r, s being Element of SAS st a <> b &amp; p,q // a,b &amp; a,b // r,s holds
p,q // r,s
proofend;

theorem :: SEMI_AF1:9
for SAS being Semi_Affine_Space
for a, b, d being Element of SAS st not a,b // a,d holds
( a <> b &amp; b <> d &amp; d <> a ) by Def1, Th1, Th3;

theorem :: SEMI_AF1:10
for SAS being Semi_Affine_Space
for a, b, p, q being Element of SAS st not a,b // p,q holds
( a <> b &amp; p <> q ) by Def1, Th3;

theorem :: SEMI_AF1:11
for SAS being Semi_Affine_Space
for a, b, x, c being Element of SAS st a,b // a,x &amp; b,c // b,x &amp; c,a // c,x holds
a,b // a,c
proofend;

theorem Th12: :: SEMI_AF1:12
for SAS being Semi_Affine_Space
for a, b, c, p, q being Element of SAS st not a,b // a,c &amp; p <> q &amp; p,q // p,a &amp; p,q // p,b holds
not p,q // p,c
proofend;

theorem Th13: :: SEMI_AF1:13
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
proofend;

theorem Th14: :: SEMI_AF1:14
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 &amp; not b,a // a,c &amp; not b,a // c,a &amp; not a,c // a,b &amp; not a,c // b,a &amp; not c,a // a,b &amp; not c,a // b,a &amp; not b,a // b,c &amp; not b,a // c,b &amp; not a,b // b,c &amp; not a,b // c,b &amp; not b,c // b,a &amp; not b,c // a,b &amp; not c,b // a,b &amp; not c,b // b,a &amp; not c,b // c,a &amp; not c,b // a,c &amp; not b,c // c,a &amp; not b,c // a,c &amp; not c,a // c,b &amp; not c,a // b,c &amp; not a,c // b,c &amp; not a,c // c,b )
proofend;

theorem Th15: :: SEMI_AF1:15
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 &amp; a,b // p,q &amp; c,d // r,s &amp; p <> q &amp; r <> s holds
not p,q // r,s
proofend;

theorem Th16: :: SEMI_AF1:16
for SAS being Semi_Affine_Space
for a, b, c, p, q, r being Element of SAS st not a,b // a,c &amp; a,b // p,q &amp; a,c // p,r &amp; b,c // q,r &amp; p <> q holds
not p,q // p,r
proofend;

theorem Th17: :: SEMI_AF1:17
for SAS being Semi_Affine_Space
for a, b, c, p, r being Element of SAS st not a,b // a,c &amp; a,c // p,r &amp; b,c // p,r holds
p = r
proofend;

theorem Th18: :: SEMI_AF1:18
for SAS being Semi_Affine_Space
for p, q, r1, r2 being Element of SAS st not p,q // p,r1 &amp; p,r1 // p,r2 &amp; q,r1 // q,r2 holds
r1 = r2
proofend;

theorem Th19: :: SEMI_AF1:19
for SAS being Semi_Affine_Space
for a, b, c, p, q, r1, r2 being Element of SAS st not a,b // a,c &amp; a,b // p,q &amp; a,c // p,r1 &amp; a,c // p,r2 &amp; b,c // q,r1 &amp; b,c // q,r2 holds
r1 = r2
proofend;

theorem :: SEMI_AF1:20
for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st ( a = b or c = d or ( a = c &amp; b = d ) or ( a = d &amp; b = c ) ) holds
a,b // c,d by Def1, Th1, Th3;

theorem :: SEMI_AF1:21
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, Th1, Th3;

::
:: BASIC FACTS ABOUT COLLINEARITY RELATION
::
definition
let SAS be Semi_Affine_Space;
let a, b, c be Element of SAS;
preda,b,c is_collinear  means :Def2: :: SEMI_AF1:def 2
a,b // a,c;
end;

:: deftheorem Def2 defines is_collinear SEMI_AF1:def_2_:_
 for SAS being Semi_Affine_Space
for a, b, c being Element of SAS holds
( a,b,c is_collinear iff a,b // a,c );

theorem Th22: :: SEMI_AF1:22
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 &amp; a2,a1,a3 is_collinear &amp; a2,a3,a1 is_collinear &amp; a3,a1,a2 is_collinear &amp; a3,a2,a1 is_collinear )
proofend;

theorem Th23: :: SEMI_AF1:23
for SAS being Semi_Affine_Space
for a, b, c, p, q, r being Element of SAS st not a,b,c is_collinear &amp; a,b // p,q &amp; a,c // p,r &amp; p <> q &amp; p <> r holds
not p,q,r is_collinear
proofend;

theorem Th24: :: SEMI_AF1:24
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
proofend;

theorem Th25: :: SEMI_AF1:25
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
proofend;

theorem Th26: :: SEMI_AF1:26
for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st a,b,c is_collinear &amp; a,b,d is_collinear holds
a,b // c,d
proofend;

theorem Th27: :: SEMI_AF1:27
for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st not a,b,c is_collinear &amp; a,b // c,d holds
not a,b,d is_collinear
proofend;

theorem Th28: :: SEMI_AF1:28
for SAS being Semi_Affine_Space
for a, b, c, d, x being Element of SAS st not a,b,c is_collinear &amp; a,b // c,d &amp; c <> d &amp; c,d,x is_collinear holds
not a,b,x is_collinear
proofend;

theorem :: SEMI_AF1:29
for SAS being Semi_Affine_Space
for o, a, b, x being Element of SAS st not o,a,b is_collinear &amp; o,a,x is_collinear &amp; o,b,x is_collinear holds
o = x
proofend;

theorem :: SEMI_AF1:30
for SAS being Semi_Affine_Space
for o, a, b, a9, b9 being Element of SAS st o <> a &amp; o <> b &amp; o,a,b is_collinear &amp; o,a,a9 is_collinear &amp; o,b,b9 is_collinear holds
a,b // a9,b9
proofend;

theorem :: SEMI_AF1:31
for SAS being Semi_Affine_Space
for a, b, c, d, p1, p2 being Element of SAS st not a,b // c,d &amp; a,b,p1 is_collinear &amp; a,b,p2 is_collinear &amp; c,d,p1 is_collinear &amp; c,d,p2 is_collinear holds
p1 = p2
proofend;

theorem Th32: :: SEMI_AF1:32
for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st a <> b &amp; a,b,c is_collinear &amp; a,b // c,d holds
a,c // b,d
proofend;

theorem Th33: :: SEMI_AF1:33
for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st a <> b &amp; a,b,c is_collinear &amp; a,b // c,d holds
c,b // c,d
proofend;

theorem Th34: :: SEMI_AF1:34
for SAS being Semi_Affine_Space
for o, a, c, b, d1, d2 being Element of SAS st not o,a,c is_collinear &amp; o,a,b is_collinear &amp; o,c,d1 is_collinear &amp; o,c,d2 is_collinear &amp; a,c // b,d1 &amp; a,c // b,d2 holds
d1 = d2
proofend;

theorem :: SEMI_AF1:35
for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st a <> b &amp; a,b,c is_collinear &amp; a,b,d is_collinear holds
a,c,d is_collinear
proofend;

::
:: PARALLELOGRAM
::
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 &amp; a,b // c,d &amp; a,c // b,d );
end;

:: deftheorem Def3 defines parallelogram SEMI_AF1:def_3_:_
 for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS holds
( parallelogram a,b,c,d iff ( not a,b,c is_collinear &amp; a,b // c,d &amp; a,c // b,d ) );

theorem Th36: :: SEMI_AF1:36
for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds
( a <> b &amp; a <> c &amp; c <> b &amp; a <> d &amp; b <> d &amp; c <> d )
proofend;

theorem Th37: :: SEMI_AF1:37
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 &amp; not b,a,d is_collinear &amp; not c,d,a is_collinear &amp; not d,c,b is_collinear )
proofend;

theorem Th38: :: SEMI_AF1:38
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 &amp; not a1,a3,a2 is_collinear &amp; not a1,a2,a4 is_collinear &amp; not a1,a4,a2 is_collinear &amp; not a1,a3,a4 is_collinear &amp; not a1,a4,a3 is_collinear &amp; not a2,a1,a3 is_collinear &amp; not a2,a3,a1 is_collinear &amp; not a2,a1,a4 is_collinear &amp; not a2,a4,a1 is_collinear &amp; not a2,a3,a4 is_collinear &amp; not a2,a4,a3 is_collinear &amp; not a3,a1,a2 is_collinear &amp; not a3,a2,a1 is_collinear &amp; not a3,a1,a4 is_collinear &amp; not a3,a4,a1 is_collinear &amp; not a3,a2,a4 is_collinear &amp; not a3,a4,a2 is_collinear &amp; not a4,a1,a2 is_collinear &amp; not a4,a2,a1 is_collinear &amp; not a4,a1,a3 is_collinear &amp; not a4,a3,a1 is_collinear &amp; not a4,a2,a3 is_collinear &amp; not a4,a3,a2 is_collinear )
proofend;

theorem Th39: :: SEMI_AF1:39
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 )
proofend;

theorem :: SEMI_AF1:40
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
proofend;

theorem :: SEMI_AF1:41
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
proofend;

theorem :: SEMI_AF1:42
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
proofend;

theorem Th43: :: SEMI_AF1:43
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 &amp; parallelogram c,d,a,b &amp; parallelogram b,a,d,c &amp; parallelogram c,a,d,b &amp; parallelogram d,b,c,a &amp; parallelogram b,d,a,c )
proofend;

theorem Th44: :: SEMI_AF1:44
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
proofend;

theorem Th45: :: SEMI_AF1:45
for SAS being Semi_Affine_Space
for a, b, c, d1, d2 being Element of SAS st parallelogram a,b,c,d1 &amp; parallelogram a,b,c,d2 holds
d1 = d2
proofend;

theorem Th46: :: SEMI_AF1:46
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
proofend;

theorem Th47: :: SEMI_AF1:47
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
proofend;

theorem Th48: :: SEMI_AF1:48
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 &amp; c <> a &amp; c <> b )
proofend;

theorem Th49: :: SEMI_AF1:49
for SAS being Semi_Affine_Space
for a, a9, b, b9, c, c9 being Element of SAS st parallelogram a,a9,b,b9 &amp; parallelogram a,a9,c,c9 holds
b,c // b9,c9
proofend;

theorem Th50: :: SEMI_AF1:50
for SAS being Semi_Affine_Space
for b, b9, c, a, a9, c9 being Element of SAS st not b,b9,c is_collinear &amp; parallelogram a,a9,b,b9 &amp; parallelogram a,a9,c,c9 holds
parallelogram b,b9,c,c9
proofend;

theorem Th51: :: SEMI_AF1:51
for SAS being Semi_Affine_Space
for a, b, c, a9, b9, c9 being Element of SAS st a,b,c is_collinear &amp; b <> c &amp; parallelogram a,a9,b,b9 &amp; parallelogram a,a9,c,c9 holds
parallelogram b,b9,c,c9
proofend;

theorem Th52: :: SEMI_AF1:52
for SAS being Semi_Affine_Space
for a, a9, b, b9, c, c9, d, d9 being Element of SAS st parallelogram a,a9,b,b9 &amp; parallelogram a,a9,c,c9 &amp; parallelogram b,b9,d,d9 holds
c,d // c9,d9
proofend;

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
proofend;

theorem :: SEMI_AF1:53
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
proofend;

::
:: CONGRUENCE
::
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 &amp; r = s ) or ex p, q being Element of SAS st
( parallelogram p,q,a,b &amp; parallelogram p,q,r,s ) );
end;

:: deftheorem Def4 defines congr SEMI_AF1:def_4_:_
 for SAS being Semi_Affine_Space
for a, b, r, s being Element of SAS holds
( congr a,b,r,s iff ( ( a = b &amp; r = s ) or ex p, q being Element of SAS st
( parallelogram p,q,a,b &amp; parallelogram p,q,r,s ) ) );

theorem Th54: :: SEMI_AF1:54
for SAS being Semi_Affine_Space
for a, b, c being Element of SAS st congr a,a,b,c holds
b = c
proofend;

theorem Th55: :: SEMI_AF1:55
for SAS being Semi_Affine_Space
for a, b, c being Element of SAS st congr a,b,c,c holds
a = b
proofend;

theorem Th56: :: SEMI_AF1:56
for SAS being Semi_Affine_Space
for a, b being Element of SAS st congr a,b,b,a holds
a = b
proofend;

theorem Th57: :: SEMI_AF1:57
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
proofend;

theorem Th58: :: SEMI_AF1:58
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
proofend;

theorem Th59: :: SEMI_AF1:59
for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st congr a,b,c,d &amp; not a,b,c is_collinear holds
parallelogram a,b,c,d
proofend;

theorem Th60: :: 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
congr a,b,c,d
proofend;

theorem Th61: :: SEMI_AF1:61
for SAS being Semi_Affine_Space
for a, b, c, d, r, s being Element of SAS st congr a,b,c,d &amp; a,b,c is_collinear &amp; parallelogram r,s,a,b holds
parallelogram r,s,c,d
proofend;

theorem Th62: :: SEMI_AF1:62
for SAS being Semi_Affine_Space
for a, b, c, x, y being Element of SAS st congr a,b,c,x &amp; congr a,b,c,y holds
x = y
proofend;

theorem Th63: :: SEMI_AF1:63
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
proofend;

theorem Th64: :: SEMI_AF1:64
for SAS being Semi_Affine_Space
for a, b being Element of SAS holds congr a,b,a,b
proofend;

theorem Th65: :: SEMI_AF1:65
for SAS being Semi_Affine_Space
for r, s, a, b, c, d being Element of SAS st congr r,s,a,b &amp; congr r,s,c,d holds
congr a,b,c,d
proofend;

theorem Th66: :: SEMI_AF1:66
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
proofend;

theorem Th67: :: SEMI_AF1:67
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
proofend;

theorem Th68: :: SEMI_AF1:68
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
proofend;

theorem Th69: :: SEMI_AF1:69
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 &amp; congr b,a,d,c &amp; congr a,c,b,d &amp; congr d,c,b,a &amp; congr b,d,a,c &amp; congr c,a,d,b &amp; congr d,b,c,a )
proofend;

theorem Th70: :: SEMI_AF1:70
for SAS being Semi_Affine_Space
for a, b, p, q, c, s being Element of SAS st congr a,b,p,q &amp; congr b,c,q,s holds
congr a,c,p,s
proofend;

theorem Th71: :: SEMI_AF1:71
for SAS being Semi_Affine_Space
for b, a, p, q, c, r being Element of SAS st congr b,a,p,q &amp; congr c,a,p,r holds
congr b,c,r,q
proofend;

theorem :: SEMI_AF1:72
for SAS being Semi_Affine_Space
for a, o, p, b, q being Element of SAS st congr a,o,o,p &amp; congr b,o,o,q holds
congr a,b,q,p by Th71;

theorem Th73: :: SEMI_AF1:73
for SAS being Semi_Affine_Space
for b, a, p, q, c, r being Element of SAS st congr b,a,p,q &amp; congr c,a,p,r holds
b,c // q,r
proofend;

theorem :: SEMI_AF1:74
for SAS being Semi_Affine_Space
for a, o, p, b, q being Element of SAS st congr a,o,o,p &amp; congr b,o,o,q holds
a,b // p,q by Th73;

::
:: A VECTOR' GROUP
::
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
existence
ex b1 being Element of SAS st congr o,a,b,b1;
uniqueness
for b1, b2 being Element of SAS st congr o,a,b,b1 &amp; congr o,a,b,b2 holds
b1 = b2;
by Th62, Th63;
end;

:: deftheorem Def5 defines sum SEMI_AF1:def_5_:_
 for SAS being Semi_Affine_Space
for a, b, o, b5 being Element of SAS holds
( b5 = sum (a,b,o) iff congr o,a,b,b5 );

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
 ex b1 being Element of SAS st sum (a,b1,o) = o
proofend;
uniqueness
 for b1, b2 being Element of SAS st sum (a,b1,o) = o &amp; sum (a,b2,o) = o holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines opposite SEMI_AF1:def_6_:_
 for SAS being Semi_Affine_Space
for a, o, b4 being Element of SAS holds
( b4 = opposite (a,o) iff sum (a,b4,o) = o );

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
coherence
sum (a,(opposite (b,o)),o) is Element of SAS;
;
end;

:: deftheorem  defines diff SEMI_AF1:def_7_:_
 for SAS being Semi_Affine_Space
for a, b, o being Element of SAS holds diff (a,b,o) = sum (a,(opposite (b,o)),o);

theorem Th75: :: SEMI_AF1:75
for SAS being Semi_Affine_Space
for a, o being Element of SAS holds sum (a,o,o) = a
proofend;

theorem :: SEMI_AF1:76
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
proofend;

theorem :: SEMI_AF1:77
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)
proofend;

theorem Th78: :: SEMI_AF1:78
for SAS being Semi_Affine_Space
for a, b, o being Element of SAS holds sum (a,b,o) = sum (b,a,o)
proofend;

theorem :: SEMI_AF1:79
for SAS being Semi_Affine_Space
for a, o being Element of SAS st sum (a,a,o) = o holds
a = o
proofend;

theorem :: SEMI_AF1:80
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
proofend;

theorem Th81: :: SEMI_AF1:81
for SAS being Semi_Affine_Space
for a, o being Element of SAS holds congr a,o,o, opposite (a,o)
proofend;

theorem Th82: :: SEMI_AF1:82
for SAS being Semi_Affine_Space
for a, o, b being Element of SAS st opposite (a,o) = opposite (b,o) holds
a = b
proofend;

theorem :: SEMI_AF1:83
for SAS being Semi_Affine_Space
for a, b, o being Element of SAS holds a,b // opposite (a,o), opposite (b,o)
proofend;

theorem :: SEMI_AF1:84
for SAS being Semi_Affine_Space
for o being Element of SAS holds opposite (o,o) = o
proofend;

theorem Th85: :: SEMI_AF1:85
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)
proofend;

theorem :: SEMI_AF1:86
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)
proofend;

theorem Th87: :: SEMI_AF1:87
for SAS being Semi_Affine_Space
for a, b, o being Element of SAS holds
( diff (a,b,o) = o iff a = b )
proofend;

theorem Th88: :: SEMI_AF1:88
for SAS being Semi_Affine_Space
for o, b, a being Element of SAS holds o, diff (b,a,o) // a,b
proofend;

theorem :: SEMI_AF1:89
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 )
proofend;

::
:: A TRAPEZIUM RELATION
::
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 &amp; o,a,b is_collinear &amp; o,c,d is_collinear &amp; a,c // b,d );
end;

:: deftheorem Def8 defines trap SEMI_AF1:def_8_:_
 for SAS being Semi_Affine_Space
for a, b, c, d, o being Element of SAS holds
( trap a,b,c,d,o iff ( not o,a,c is_collinear &amp; o,a,b is_collinear &amp; o,c,d is_collinear &amp; a,c // b,d ) );

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 &amp; p,c // b,d ) );
end;

:: deftheorem Def9 defines qtrap SEMI_AF1:def_9_:_
 for SAS being Semi_Affine_Space
for o, p being Element of SAS holds
( qtrap o,p iff 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 &amp; p,c // b,d ) ) );

theorem Th90: :: SEMI_AF1:90
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 &amp; a <> c &amp; c <> o )
proofend;

theorem :: SEMI_AF1:91
for SAS being Semi_Affine_Space
for a, b, c, x, o, y being Element of SAS st trap a,b,c,x,o &amp; trap a,b,c,y,o holds
x = y
proofend;

theorem :: SEMI_AF1:92
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
proofend;

theorem Th93: :: SEMI_AF1:93
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
proofend;

theorem Th94: :: SEMI_AF1:94
for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st trap a,b,c,d,d holds
d = b
proofend;

theorem Th95: :: SEMI_AF1:95
for SAS being Semi_Affine_Space
for o, b, a, c, d being Element of SAS st o <> b &amp; trap a,b,c,d,o holds
not o,b,d is_collinear
proofend;

theorem :: SEMI_AF1:96
for SAS being Semi_Affine_Space
for o, b, a, c, d being Element of SAS st o <> b &amp; trap a,b,c,d,o holds
trap b,a,d,c,o
proofend;

theorem :: SEMI_AF1:97
for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st trap a,b,c,d,b holds
b = d by Th93, Th94;

theorem Th98: :: SEMI_AF1:98
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 &amp; trap a,p,c,r,o holds
b,c // q,r
proofend;

theorem Th99: :: SEMI_AF1:99
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 &amp; trap a,p,c,r,o &amp; not o,b,c is_collinear holds
trap b,q,c,r,o
proofend;

theorem :: SEMI_AF1:100
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 &amp; trap a,p,c,r,o &amp; trap b,q,d,s,o holds
c,d // r,s
proofend;

theorem Th101: :: SEMI_AF1:101
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 &amp; qtrap o,p )
proofend;

theorem Th102: :: SEMI_AF1:102
for SAS being Semi_Affine_Space ex x, y, z being Element of SAS st
( x <> y &amp; y <> z &amp; z <> x )
proofend;

theorem Th103: :: SEMI_AF1:103
for SAS being Semi_Affine_Space
for o, p being Element of SAS st qtrap o,p holds
o <> p
proofend;

theorem :: SEMI_AF1:104
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 &amp; qtrap o,q )
proofend;

theorem :: SEMI_AF1:105
for SAS being Semi_Affine_Space
for o, p, c, b being Element of SAS st not o,p,c is_collinear &amp; o,p,b is_collinear &amp; qtrap o,p holds
ex d being Element of SAS st trap p,b,c,d,o
proofend;