:: SEMI_AF1 semantic presentation

definition

let c₁ be non empty AffinStruct ;
attr a₁ is Semi_Affine_Space-like means :Def1: :: SEMI_AF1:def 1
( ( for b₁, b₂ being Element of a₁ holds b₁,b₂ // b₂,b₁ ) & ( for b₁, b₂, b₃ being Element of a₁ holds b₁,b₂ // b₃,b₃ ) & ( for b₁, b₂, b₃, b₄, b₅, b₆ being Element of a₁ st b₁ <> b₂ & b₁,b₂ // b₃,b₄ & b₁,b₂ // b₅,b₆ holds
b₃,b₄ // b₅,b₆ ) & ( for b₁, b₂, b₃ being Element of a₁ st b₁,b₂ // b₁,b₃ holds
b₂,b₁ // b₂,b₃ ) & not for b₁, b₂, b₃ being Element of a₁ holds b₁,b₂ // b₁,b₃ & ( for b₁, b₂, b₃ being Element of a₁ ex b₄ being Element of a₁ st
( b₁,b₂ // b₃,b₄ & b₁,b₃ // b₂,b₄ ) ) & ( for b₁, b₂ being Element of a₁ ex b₃ being Element of a₁ st
for b₄, b₅ being Element of a₁ holds
( b₁,b₂ // b₁,b₃ & ex b₆ being Element of a₁ st
( b₁,b₃ // b₁,b₄ implies ( b₁,b₅ // b₁,b₆ & b₃,b₅ // b₄,b₆ ) ) ) ) & ( for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being Element of a₁ st not b₁,b₂ // b₁,b₄ & not b₁,b₂ // b₁,b₆ & b₁,b₂ // b₁,b₃ & b₁,b₄ // b₁,b₅ & b₁,b₆ // b₁,b₇ & b₂,b₄ // b₃,b₅ & b₂,b₆ // b₃,b₇ holds
b₄,b₆ // b₅,b₇ ) & ( for b₁, b₂, b₃, b₄, b₅, b₆ being Element of a₁ st not b₁,b₂ // b₁,b₃ & not b₁,b₂ // b₁,b₅ & b₁,b₂ // b₃,b₄ & b₁,b₂ // b₅,b₆ & b₁,b₃ // b₂,b₄ & b₁,b₅ // b₂,b₆ holds
b₃,b₅ // b₄,b₆ ) & ( for b₁, b₂, b₃, b₄, b₅, b₆ being Element of a₁ st b₁,b₂ // b₁,b₃ & b₄,b₅ // b₄,b₆ & b₁,b₅ // b₂,b₄ & b₂,b₆ // b₃,b₅ holds
b₃,b₄ // b₁,b₆ ) & ( for b₁, b₂, b₃, b₄ being Element of a₁ st not b₁,b₂ // b₁,b₃ & b₁,b₂ // b₃,b₄ & b₁,b₃ // b₂,b₄ holds
not b₁,b₄ // b₂,b₃ ) );

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 Th1: :: SEMI_AF1:1

canceled;

theorem Th2: :: SEMI_AF1:2

canceled;

theorem Th3: :: SEMI_AF1:3

canceled;

theorem Th4: :: SEMI_AF1:4

canceled;

theorem Th5: :: SEMI_AF1:5

canceled;

theorem Th6: :: SEMI_AF1:6

canceled;

theorem Th7: :: SEMI_AF1:7

canceled;

theorem Th8: :: SEMI_AF1:8

canceled;

theorem Th9: :: SEMI_AF1:9

canceled;

theorem Th10: :: SEMI_AF1:10

canceled;

theorem Th11: :: SEMI_AF1:11

canceled;

theorem Th12: :: SEMI_AF1:12

for b₁ being Semi_Affine_Space
for b₂, b₃ being Element of b₁ holds b₂,b₃ // b₂,b₃

proof end;

theorem Th13: :: SEMI_AF1:13

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₄,b₅ holds
b₄,b₅ // b₂,b₃

proof end;

theorem Th14: :: SEMI_AF1:14

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄ being Element of b₁ holds b₂,b₂ // b₃,b₄

proof end;

theorem Th15: :: SEMI_AF1:15

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₄,b₅ holds
b₃,b₂ // b₄,b₅

proof end;

theorem Th16: :: SEMI_AF1:16

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₄,b₅ holds
b₂,b₃ // b₅,b₄

proof end;

theorem Th17: :: SEMI_AF1:17

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₄,b₅ holds
( b₃,b₂ // b₄,b₅ & b₂,b₃ // b₅,b₄ & b₃,b₂ // b₅,b₄ & b₄,b₅ // b₂,b₃ & b₅,b₄ // b₂,b₃ & b₄,b₅ // b₃,b₂ & b₅,b₄ // b₃,b₂ )

proof end;

theorem Th18: :: SEMI_AF1:18

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄ being Element of b₁ st b₂,b₃ // b₂,b₄ holds
( b₂,b₄ // b₂,b₃ & b₃,b₂ // b₂,b₄ & b₂,b₃ // b₄,b₂ & b₂,b₄ // b₃,b₂ & b₃,b₂ // b₄,b₂ & b₄,b₂ // b₂,b₃ & b₄,b₂ // b₃,b₂ & b₃,b₂ // b₃,b₄ & b₂,b₃ // b₃,b₄ & b₃,b₂ // b₄,b₃ & b₃,b₄ // b₃,b₂ & b₂,b₃ // b₄,b₃ & b₄,b₃ // b₃,b₂ & b₃,b₄ // b₂,b₃ & b₄,b₃ // b₂,b₃ & b₄,b₂ // b₄,b₃ & b₂,b₄ // b₄,b₃ & b₄,b₂ // b₃,b₄ & b₂,b₄ // b₃,b₄ & b₄,b₃ // b₄,b₂ & b₃,b₄ // b₄,b₂ & b₄,b₃ // b₂,b₄ & b₃,b₄ // b₂,b₄ )

proof end;

theorem Th19: :: SEMI_AF1:19

canceled;

theorem Th20: :: SEMI_AF1:20

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂ <> b₃ & b₄,b₅ // b₂,b₃ & b₂,b₃ // b₆,b₇ holds
b₄,b₅ // b₆,b₇

proof end;

theorem Th21: :: SEMI_AF1:21

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄ being Element of b₁ st not b₂,b₃ // b₂,b₄ holds
( b₂ <> b₃ & b₃ <> b₄ & b₄ <> b₂ ) by Def1, Th12, Th14;

theorem Th22: :: SEMI_AF1:22

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st not b₂,b₃ // b₄,b₅ holds
( b₂ <> b₃ & b₄ <> b₅ ) by Def1, Th14;

theorem Th23: :: SEMI_AF1:23

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₂,b₄ & b₃,b₅ // b₃,b₄ & b₅,b₂ // b₅,b₄ holds
b₂,b₃ // b₂,b₅

proof end;

theorem Th24: :: SEMI_AF1:24

canceled;

theorem Th25: :: SEMI_AF1:25

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not b₂,b₃ // b₂,b₄ & b₅ <> b₆ & b₅,b₆ // b₅,b₂ & b₅,b₆ // b₅,b₃ holds
not b₅,b₆ // b₅,b₄

proof end;

theorem Th26: :: SEMI_AF1:26

for b₁ being Semi_Affine_Space
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
ex b₄ being Element of b₁ st not b₂,b₃ // b₂,b₄

proof end;

theorem Th27: :: SEMI_AF1:27

canceled;

theorem Th28: :: SEMI_AF1:28

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄ being Element of b₁ st not b₂,b₃ // b₂,b₄ holds
( not b₂,b₃ // b₄,b₂ & not b₃,b₂ // b₂,b₄ & not b₃,b₂ // b₄,b₂ & not b₂,b₄ // b₂,b₃ & not b₂,b₄ // b₃,b₂ & not b₄,b₂ // b₂,b₃ & not b₄,b₂ // b₃,b₂ & not b₃,b₂ // b₃,b₄ & not b₃,b₂ // b₄,b₃ & not b₂,b₃ // b₃,b₄ & not b₂,b₃ // b₄,b₃ & not b₃,b₄ // b₃,b₂ & not b₃,b₄ // b₂,b₃ & not b₄,b₃ // b₂,b₃ & not b₄,b₃ // b₃,b₂ & not b₄,b₃ // b₄,b₂ & not b₄,b₃ // b₂,b₄ & not b₃,b₄ // b₄,b₂ & not b₃,b₄ // b₂,b₄ & not b₄,b₂ // b₄,b₃ & not b₄,b₂ // b₃,b₄ & not b₂,b₄ // b₃,b₄ & not b₂,b₄ // b₄,b₃ )

proof end;

theorem Th29: :: SEMI_AF1:29

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉ being Element of b₁ st not b₂,b₃ // b₄,b₅ & b₂,b₃ // b₆,b₇ & b₄,b₅ // b₈,b₉ & b₆ <> b₇ & b₈ <> b₉ holds
not b₆,b₇ // b₈,b₉

proof end;

theorem Th30: :: SEMI_AF1:30

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st not b₂,b₃ // b₂,b₄ & b₂,b₃ // b₅,b₆ & b₂,b₄ // b₅,b₇ & b₃,b₄ // b₆,b₇ & b₅ <> b₆ holds
not b₅,b₆ // b₅,b₇

proof end;

theorem Th31: :: SEMI_AF1:31

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not b₂,b₃ // b₂,b₄ & b₂,b₄ // b₅,b₆ & b₃,b₄ // b₅,b₆ holds
b₅ = b₆

proof end;

theorem Th32: :: SEMI_AF1:32

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st not b₂,b₃ // b₂,b₄ & b₂,b₄ // b₂,b₅ & b₃,b₄ // b₃,b₅ holds
b₄ = b₅

proof end;

theorem Th33: :: SEMI_AF1:33

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁ st not b₂,b₃ // b₂,b₄ & b₂,b₃ // b₅,b₆ & b₂,b₄ // b₅,b₇ & b₂,b₄ // b₅,b₈ & b₃,b₄ // b₆,b₇ & b₃,b₄ // b₆,b₈ holds
b₇ = b₈

proof end;

theorem Th34: :: SEMI_AF1:34

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st ( b₂ = b₃ or b₄ = b₅ or ( b₂ = b₄ & b₃ = b₅ ) or ( b₂ = b₅ & b₃ = b₄ ) ) holds
b₂,b₃ // b₄,b₅ by Def1, Th12, Th14;

theorem Th35: :: SEMI_AF1:35

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄ being Element of b₁ st ( b₂ = b₃ or b₂ = b₄ or b₃ = b₄ ) holds
b₂,b₃ // b₂,b₄ by Def1, Th12, Th14;

definition

let c₁ be Semi_Affine_Space;
let c₂, c₃, c₄ be Element of c₁;
pred c₂,c₃,c₄ is_collinear means :Def2: :: SEMI_AF1:def 2
a₂,a₃ // a₂,a₄;

end;

:: deftheorem Def2 defines is_collinear SEMI_AF1:def 2 :

theorem Th36: :: SEMI_AF1:36

canceled;

theorem Th37: :: SEMI_AF1:37

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄ being Element of b₁ st b₂,b₃,b₄ is_collinear holds
( b₂,b₄,b₃ is_collinear & b₃,b₂,b₄ is_collinear & b₃,b₄,b₂ is_collinear & b₄,b₂,b₃ is_collinear & b₄,b₃,b₂ is_collinear )

proof end;

theorem Th38: :: SEMI_AF1:38

canceled;

theorem Th39: :: SEMI_AF1:39

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃ // b₅,b₆ & b₂,b₄ // b₅,b₇ & b₅ <> b₆ & b₅ <> b₇ holds
not b₅,b₆,b₇ is_collinear

proof end;

theorem Th40: :: SEMI_AF1:40

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄ being Element of b₁ st ( b₂ = b₃ or b₃ = b₄ or b₄ = b₂ ) holds
b₂,b₃,b₄ is_collinear

proof end;

theorem Th41: :: SEMI_AF1:41

for b₁ being Semi_Affine_Space
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
ex b₄ being Element of b₁ st not b₂,b₃,b₄ is_collinear

proof end;

theorem Th42: :: SEMI_AF1:42

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear holds
b₂,b₃ // b₄,b₅

proof end;

theorem Th43: :: SEMI_AF1:43

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃ // b₄,b₅ holds
not b₂,b₃,b₅ is_collinear

proof end;

theorem Th44: :: SEMI_AF1:44

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃ // b₄,b₅ & b₄ <> b₅ & b₄,b₅,b₆ is_collinear holds
not b₂,b₃,b₆ is_collinear

proof end;

theorem Th45: :: SEMI_AF1:45

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & b₂,b₄,b₅ is_collinear holds
b₂ = b₅

proof end;

theorem Th46: :: SEMI_AF1:46

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂ <> b₃ & b₂ <> b₄ & b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & b₂,b₄,b₆ is_collinear holds
b₃,b₄ // b₅,b₆

proof end;

theorem Th47: :: SEMI_AF1:47

canceled;

theorem Th48: :: SEMI_AF1:48

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st not b₂,b₃ // b₄,b₅ & b₂,b₃,b₆ is_collinear & b₂,b₃,b₇ is_collinear & b₄,b₅,b₆ is_collinear & b₄,b₅,b₇ is_collinear holds
b₆ = b₇

proof end;

theorem Th49: :: SEMI_AF1:49

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <> b₃ & b₂,b₃,b₄ is_collinear & b₂,b₃ // b₄,b₅ holds
b₂,b₄ // b₃,b₅

proof end;

theorem Th50: :: SEMI_AF1:50

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <> b₃ & b₂,b₃,b₄ is_collinear & b₂,b₃ // b₄,b₅ holds
b₄,b₃ // b₄,b₅

proof end;

theorem Th51: :: SEMI_AF1:51

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & b₂,b₄,b₆ is_collinear & b₂,b₄,b₇ is_collinear & b₃,b₄ // b₅,b₆ & b₃,b₄ // b₅,b₆ & b₃,b₄ // b₅,b₇ holds
b₆ = b₇

proof end;

theorem Th52: :: SEMI_AF1:52

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <> b₃ & b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear holds
b₂,b₄,b₅ is_collinear

proof end;

definition

let c₁ be Semi_Affine_Space;
let c₂, c₃, c₄, c₅ be Element of c₁;
pred parallelogram c₂,c₃,c₄,c₅ means :Def3: :: SEMI_AF1:def 3
( not a₂,a₃,a₄ is_collinear & a₂,a₃ // a₄,a₅ & a₂,a₄ // a₃,a₅ );

end;

:: deftheorem Def3 defines parallelogram SEMI_AF1:def 3 :

theorem Th53: :: SEMI_AF1:53

canceled;

theorem Th54: :: SEMI_AF1:54

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
( b₂ <> b₃ & b₂ <> b₄ & b₄ <> b₃ & b₂ <> b₅ & b₃ <> b₅ & b₄ <> b₅ )

proof end;

theorem Th55: :: SEMI_AF1:55

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
( not b₂,b₃,b₄ is_collinear & not b₃,b₂,b₅ is_collinear & not b₄,b₅,b₂ is_collinear & not b₅,b₄,b₃ is_collinear )

proof end;

theorem Th56: :: SEMI_AF1:56

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
( not b₂,b₃,b₄ is_collinear & not b₂,b₄,b₃ is_collinear & not b₂,b₃,b₅ is_collinear & not b₂,b₅,b₃ is_collinear & not b₂,b₄,b₅ is_collinear & not b₂,b₅,b₄ is_collinear & not b₃,b₂,b₄ is_collinear & not b₃,b₄,b₂ is_collinear & not b₃,b₂,b₅ is_collinear & not b₃,b₅,b₂ is_collinear & not b₃,b₄,b₅ is_collinear & not b₃,b₅,b₄ is_collinear & not b₄,b₂,b₃ is_collinear & not b₄,b₃,b₂ is_collinear & not b₄,b₂,b₅ is_collinear & not b₄,b₅,b₂ is_collinear & not b₄,b₃,b₅ is_collinear & not b₄,b₅,b₃ is_collinear & not b₅,b₂,b₃ is_collinear & not b₅,b₃,b₂ is_collinear & not b₅,b₂,b₄ is_collinear & not b₅,b₄,b₂ is_collinear & not b₅,b₃,b₄ is_collinear & not b₅,b₄,b₃ is_collinear )

proof end;

theorem Th57: :: SEMI_AF1:57

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ holds
( not parallelogram b₂,b₃,b₄,b₅ or not b₂,b₃,b₆ is_collinear or not b₄,b₅,b₆ is_collinear )

proof end;

theorem Th58: :: SEMI_AF1:58

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
parallelogram b₂,b₄,b₃,b₅

proof end;

theorem Th59: :: SEMI_AF1:59

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
parallelogram b₄,b₅,b₂,b₃

proof end;

theorem Th60: :: SEMI_AF1:60

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
parallelogram b₃,b₂,b₅,b₄

proof end;

theorem Th61: :: SEMI_AF1:61

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
( parallelogram b₂,b₄,b₃,b₅ & parallelogram b₄,b₅,b₂,b₃ & parallelogram b₃,b₂,b₅,b₄ & parallelogram b₄,b₂,b₅,b₃ & parallelogram b₅,b₃,b₄,b₂ & parallelogram b₃,b₅,b₂,b₄ )

proof end;

theorem Th62: :: SEMI_AF1:62

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄ being Element of b₁ st not b₂,b₃,b₄ is_collinear holds
ex b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅

proof end;

theorem Th63: :: SEMI_AF1:63

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ & parallelogram b₂,b₃,b₄,b₆ holds
b₅ = b₆

proof end;

theorem Th64: :: SEMI_AF1:64

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
not b₂,b₅ // b₃,b₄

proof end;

theorem Th65: :: SEMI_AF1:65

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
not parallelogram b₂,b₃,b₅,b₄

proof end;

theorem Th66: :: SEMI_AF1:66

for b₁ being Semi_Affine_Space
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
ex b₄ being Element of b₁ st
( b₂,b₃,b₄ is_collinear & b₄ <> b₂ & b₄ <> b₃ )

proof end;

theorem Th67: :: SEMI_AF1:67

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ & parallelogram b₂,b₃,b₆,b₇ holds
b₄,b₆ // b₅,b₇

proof end;

theorem Th68: :: SEMI_AF1:68

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st not b₂,b₃,b₄ is_collinear & parallelogram b₅,b₆,b₂,b₃ & parallelogram b₅,b₆,b₄,b₇ holds
parallelogram b₂,b₃,b₄,b₇

proof end;

theorem Th69: :: SEMI_AF1:69

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂,b₃,b₄ is_collinear & b₃ <> b₄ & parallelogram b₂,b₅,b₃,b₆ & parallelogram b₂,b₅,b₄,b₇ holds
parallelogram b₃,b₆,b₄,b₇

proof end;

theorem Th70: :: SEMI_AF1:70

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ & parallelogram b₂,b₃,b₆,b₇ & parallelogram b₄,b₅,b₈,b₉ holds
b₆,b₈ // b₇,b₉

proof end;

Lemma44: for b₁ being Semi_Affine_Space
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
ex b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅

proof end;

theorem Th71: :: SEMI_AF1:71

for b₁ being Semi_Affine_Space
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
ex b₄, b₅ being Element of b₁ st parallelogram b₂,b₄,b₅,b₃

proof end;

definition

let c₁ be Semi_Affine_Space;
let c₂, c₃, c₄, c₅ be Element of c₁;
pred congr c₂,c₃,c₄,c₅ means :Def4: :: SEMI_AF1:def 4
( ( a₂ = a₃ & a₄ = a₅ ) or ex b₁, b₂ being Element of a₁ st
( parallelogram b₁,b₂,a₂,a₃ & parallelogram b₁,b₂,a₄,a₅ ) );

end;

:: deftheorem Def4 defines congr SEMI_AF1:def 4 :

theorem Th72: :: SEMI_AF1:72

canceled;

theorem Th73: :: SEMI_AF1:73

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄ being Element of b₁ st congr b₂,b₂,b₃,b₄ holds
b₃ = b₄

proof end;

theorem Th74: :: SEMI_AF1:74

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄ being Element of b₁ st congr b₂,b₃,b₄,b₄ holds
b₂ = b₃

proof end;

theorem Th75: :: SEMI_AF1:75

for b₁ being Semi_Affine_Space
for b₂, b₃ being Element of b₁ st congr b₂,b₃,b₃,b₂ holds
b₂ = b₃

proof end;

theorem Th76: :: SEMI_AF1:76

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st congr b₂,b₃,b₄,b₅ holds
b₂,b₃ // b₄,b₅

proof end;

theorem Th77: :: SEMI_AF1:77

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st congr b₂,b₃,b₄,b₅ holds
b₂,b₄ // b₃,b₅

proof end;

theorem Th78: :: SEMI_AF1:78

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st congr b₂,b₃,b₄,b₅ & not b₂,b₃,b₄ is_collinear holds
parallelogram b₂,b₃,b₄,b₅

proof end;

theorem Th79: :: SEMI_AF1:79

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
congr b₂,b₃,b₄,b₅

proof end;

theorem Th80: :: SEMI_AF1:80

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st congr b₂,b₃,b₄,b₅ & b₂,b₃,b₄ is_collinear & parallelogram b₆,b₇,b₂,b₃ holds
parallelogram b₆,b₇,b₄,b₅

proof end;

theorem Th81: :: SEMI_AF1:81

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st congr b₂,b₃,b₄,b₅ & congr b₂,b₃,b₄,b₆ holds
b₅ = b₆

proof end;

theorem Th82: :: SEMI_AF1:82

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄ being Element of b₁ ex b₅ being Element of b₁ st congr b₂,b₃,b₄,b₅

proof end;

theorem Th83: :: SEMI_AF1:83

canceled;

theorem Th84: :: SEMI_AF1:84

for b₁ being Semi_Affine_Space
for b₂, b₃ being Element of b₁ holds congr b₂,b₃,b₂,b₃

proof end;

theorem Th85: :: SEMI_AF1:85

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st congr b₂,b₃,b₄,b₅ & congr b₂,b₃,b₆,b₇ holds
congr b₄,b₅,b₆,b₇

proof end;

theorem Th86: :: SEMI_AF1:86

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st congr b₂,b₃,b₄,b₅ holds
congr b₄,b₅,b₂,b₃

proof end;

theorem Th87: :: SEMI_AF1:87

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st congr b₂,b₃,b₄,b₅ holds
congr b₃,b₂,b₅,b₄

proof end;

theorem Th88: :: SEMI_AF1:88

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st congr b₂,b₃,b₄,b₅ holds
congr b₂,b₄,b₃,b₅

proof end;

theorem Th89: :: SEMI_AF1:89

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st congr b₂,b₃,b₄,b₅ holds
( congr b₄,b₅,b₂,b₃ & congr b₃,b₂,b₅,b₄ & congr b₂,b₄,b₃,b₅ & congr b₅,b₄,b₃,b₂ & congr b₃,b₅,b₂,b₄ & congr b₄,b₂,b₅,b₃ & congr b₅,b₃,b₄,b₂ )

proof end;

theorem Th90: :: SEMI_AF1:90

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st congr b₂,b₃,b₄,b₅ & congr b₃,b₆,b₅,b₇ holds
congr b₂,b₆,b₄,b₇

proof end;

theorem Th91: :: SEMI_AF1:91

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st congr b₂,b₃,b₄,b₅ & congr b₆,b₃,b₄,b₇ holds
congr b₂,b₆,b₇,b₅

proof end;

theorem Th92: :: SEMI_AF1:92

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st congr b₂,b₃,b₃,b₄ & congr b₅,b₃,b₃,b₆ holds
congr b₂,b₅,b₆,b₄ by Th91;

theorem Th93: :: SEMI_AF1:93

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st congr b₂,b₃,b₄,b₅ & congr b₆,b₃,b₄,b₇ holds
b₂,b₆ // b₅,b₇

proof end;

theorem Th94: :: SEMI_AF1:94

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st congr b₂,b₃,b₃,b₄ & congr b₅,b₃,b₃,b₆ holds
b₂,b₅ // b₄,b₆ by Th93;

definition

let c₁ be Semi_Affine_Space;
let c₂, c₃, c₄ be Element of c₁;
func sum c₂,c₃,c₄ -> Element of a₁ means :Def5: :: SEMI_AF1:def 5
congr a₄,a₂,a₃,a₅;
correctness by Th81, Th82;

end;

:: deftheorem Def5 defines sum SEMI_AF1:def 5 :

definition

let c₁ be Semi_Affine_Space;
let c₂, c₃ be Element of c₁;
func opposite c₂,c₃ -> Element of a₁ means :Def6: :: SEMI_AF1:def 6
sum a₂,a₄,a₃ = a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines opposite SEMI_AF1:def 6 :

definition

let c₁ be Semi_Affine_Space;
let c₂, c₃, c₄ be Element of c₁;
func diff c₂,c₃,c₄ -> Element of a₁ equals :: SEMI_AF1:def 7
sum a₂,(opposite a₃,a₄),a₄;
correctness ;

end;

:: deftheorem Def7 defines diff SEMI_AF1:def 7 :

theorem Th95: :: SEMI_AF1:95

canceled;

theorem Th96: :: SEMI_AF1:96

canceled;

theorem Th97: :: SEMI_AF1:97

canceled;

theorem Th98: :: SEMI_AF1:98

canceled;

theorem Th99: :: SEMI_AF1:99

for b₁ being Semi_Affine_Space
for b₂, b₃ being Element of b₁ holds sum b₂,b₃,b₃ = b₂

proof end;

theorem Th100: :: SEMI_AF1:100

for b₁ being Semi_Affine_Space
for b₂, b₃ being Element of b₁ ex b₄ being Element of b₁ st sum b₂,b₄,b₃ = b₃

proof end;

theorem Th101: :: SEMI_AF1:101

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ holds sum (sum b₂,b₃,b₄),b₅,b₄ = sum b₂,(sum b₃,b₅,b₄),b₄

proof end;

theorem Th102: :: SEMI_AF1:102

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄ being Element of b₁ holds sum b₂,b₃,b₄ = sum b₃,b₂,b₄

proof end;

theorem Th103: :: SEMI_AF1:103

for b₁ being Semi_Affine_Space
for b₂, b₃ being Element of b₁ st sum b₂,b₂,b₃ = b₃ holds
b₂ = b₃

proof end;

theorem Th104: :: SEMI_AF1:104

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st sum b₂,b₃,b₄ = sum b₂,b₅,b₄ holds
b₃ = b₅

proof end;

theorem Th105: :: SEMI_AF1:105

canceled;

theorem Th106: :: SEMI_AF1:106

for b₁ being Semi_Affine_Space
for b₂, b₃ being Element of b₁ holds congr b₂,b₃,b₃, opposite b₂,b₃

proof end;

theorem Th107: :: SEMI_AF1:107

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄ being Element of b₁ st opposite b₂,b₃ = opposite b₄,b₃ holds
b₂ = b₄

proof end;

theorem Th108: :: SEMI_AF1:108

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄ being Element of b₁ holds b₂,b₃ // opposite b₂,b₄, opposite b₃,b₄

proof end;

theorem Th109: :: SEMI_AF1:109

for b₁ being Semi_Affine_Space
for b₂ being Element of b₁ holds opposite b₂,b₂ = b₂

proof end;

theorem Th110: :: SEMI_AF1:110

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ holds b₂,b₃ // sum b₂,b₄,b₅, sum b₃,b₄,b₅

proof end;

theorem Th111: :: SEMI_AF1:111

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂,b₃ // b₄,b₅ holds
b₂,b₃ // sum b₂,b₄,b₆, sum b₃,b₅,b₆

proof end;

theorem Th112: :: SEMI_AF1:112

canceled;

theorem Th113: :: SEMI_AF1:113

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄ being Element of b₁ holds
( diff b₂,b₃,b₄ = b₄ iff b₂ = b₃ )

proof end;

theorem Th114: :: SEMI_AF1:114

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄ being Element of b₁ holds b₂, diff b₃,b₄,b₂ // b₄,b₃

proof end;

theorem Th115: :: SEMI_AF1:115

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ holds
( b₂, diff b₃,b₄,b₂, diff b₅,b₆,b₂ is_collinear iff b₄,b₃ // b₆,b₅ )

proof end;

definition

let c₁ be Semi_Affine_Space;
let c₂, c₃, c₄, c₅, c₆ be Element of c₁;
pred trap c₂,c₃,c₄,c₅,c₆ means :Def8: :: SEMI_AF1:def 8
( not a₆,a₂,a₄ is_collinear & a₆,a₂,a₃ is_collinear & a₆,a₄,a₅ is_collinear & a₂,a₄ // a₃,a₅ );

end;

:: deftheorem Def8 defines trap SEMI_AF1:def 8 :

definition

let c₁ be Semi_Affine_Space;
let c₂, c₃ be Element of c₁;
pred qtrap c₂,c₃ means :Def9: :: SEMI_AF1:def 9
for b₁, b₂ being Element of a₁ ex b₃ being Element of a₁ st
( a₂,a₃,b₁ is_collinear implies ( a₂,b₂,b₃ is_collinear & a₃,b₂ // b₁,b₃ ) );

end;

:: deftheorem Def9 defines qtrap SEMI_AF1:def 9 :

theorem Th116: :: SEMI_AF1:116

canceled;

theorem Th117: :: SEMI_AF1:117

canceled;

theorem Th118: :: SEMI_AF1:118

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st trap b₂,b₃,b₄,b₅,b₆ holds
( b₆ <> b₂ & b₂ <> b₄ & b₄ <> b₆ )

proof end;

theorem Th119: :: SEMI_AF1:119

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st trap b₂,b₃,b₄,b₅,b₆ & trap b₂,b₃,b₄,b₇,b₆ holds
b₅ = b₇

proof end;

theorem Th120: :: SEMI_AF1:120

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄ being Element of b₁ st not b₂,b₃,b₄ is_collinear holds
trap b₃,b₂,b₄,b₂,b₂

proof end;

theorem Th121: :: SEMI_AF1:121

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st trap b₂,b₃,b₄,b₅,b₆ holds
trap b₄,b₅,b₂,b₃,b₆

proof end;

theorem Th122: :: SEMI_AF1:122

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂ <> b₃ & trap b₄,b₃,b₅,b₆,b₂ holds
b₂ <> b₆

proof end;

theorem Th123: :: SEMI_AF1:123

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂ <> b₃ & trap b₄,b₃,b₅,b₆,b₂ holds
not b₂,b₃,b₆ is_collinear

proof end;

theorem Th124: :: SEMI_AF1:124

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂ <> b₃ & trap b₄,b₃,b₅,b₆,b₂ holds
trap b₃,b₄,b₆,b₅,b₂

proof end;

theorem Th125: :: SEMI_AF1:125

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st ( b₂ = b₃ or b₂ = b₄ ) & trap b₅,b₃,b₆,b₄,b₂ holds
( b₂ = b₃ & b₂ = b₄ )

proof end;

theorem Th126: :: SEMI_AF1:126

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁ st trap b₂,b₃,b₄,b₅,b₆ & trap b₂,b₃,b₇,b₈,b₆ holds
b₄,b₇ // b₅,b₈

proof end;

theorem Th127: :: SEMI_AF1:127

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁ st trap b₂,b₃,b₄,b₅,b₆ & trap b₂,b₃,b₇,b₈,b₆ & not b₆,b₄,b₇ is_collinear holds
trap b₄,b₅,b₇,b₈,b₆

proof end;

theorem Th128: :: SEMI_AF1:128

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of b₁ st trap b₂,b₃,b₄,b₅,b₆ & trap b₂,b₃,b₇,b₈,b₆ & trap b₄,b₅,b₉,b₁₀,b₆ holds
b₇,b₉ // b₈,b₁₀

proof end;

theorem Th129: :: SEMI_AF1:129

for b₁ being Semi_Affine_Space
for b₂, b₃ being Element of b₁ ex b₄ being Element of b₁ st
( b₂,b₃,b₄ is_collinear & qtrap b₂,b₄ )

proof end;

theorem Th130: :: SEMI_AF1:130

for b₁ being Semi_Affine_Space ex b₂, b₃, b₄ being Element of b₁ st
( b₂ <> b₃ & b₃ <> b₄ & b₄ <> b₂ )

proof end;

theorem Th131: :: SEMI_AF1:131

for b₁ being Semi_Affine_Space
for b₂, b₃ being Element of b₁ st qtrap b₂,b₃ holds
b₂ <> b₃

proof end;

theorem Th132: :: SEMI_AF1:132

for b₁ being Semi_Affine_Space
for b₂, b₃ being Element of b₁ st qtrap b₂,b₃ holds
ex b₄ being Element of b₁ st
( not b₂,b₃,b₄ is_collinear & qtrap b₂,b₄ )

proof end;

theorem Th133: :: SEMI_AF1:133

for b₁ being Semi_Affine_Space
for b₂, b₃, b₄, b₅ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & qtrap b₂,b₃ holds
ex b₆ being Element of b₁ st trap b₃,b₅,b₄,b₆,b₂

proof end;