:: AFF_4 semantic presentation

Lemma1: for b₁ being AffinSpace
for b₂ being Subset of b₁
for b₃ being set st b₃ in b₂ holds
b₃ is Element of b₁
;

theorem Th1: :: AFF_4:1

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st ( LIN b₂,b₃,b₄ or LIN b₂,b₄,b₃ ) & b₂ <> b₃ holds
ex b₆ being Element of b₁ st
( LIN b₂,b₅,b₆ & b₃,b₅ // b₄,b₆ )

proof end;

theorem Th2: :: AFF_4:2

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ st ( b₂,b₃ // b₄ or b₃,b₂ // b₄ ) & b₂ in b₄ holds
b₃ in b₄

proof end;

theorem Th3: :: AFF_4:3

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

proof end;

theorem Th4: :: AFF_4:4

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆ being Subset of b₁ st ( b₂,b₃ // b₆ or b₃,b₂ // b₆ ) & ( b₂,b₃ // b₄,b₅ or b₄,b₅ // b₂,b₃ ) & b₂ <> b₃ holds
( b₄,b₅ // b₆ & b₅,b₄ // b₆ )

proof end;

theorem Th5: :: AFF_4:5

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄, b₅ being Subset of b₁ st ( b₂,b₃ // b₄ or b₃,b₂ // b₄ ) & ( b₂,b₃ // b₅ or b₃,b₂ // b₅ ) & b₂ <> b₃ holds
( b₄ // b₅ & b₅ // b₄ )

proof end;

theorem Th6: :: AFF_4:6

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆ being Subset of b₁ st ( b₂,b₃ // b₆ or b₃,b₂ // b₆ ) & ( b₄,b₅ // b₆ or b₅,b₄ // b₆ ) holds
( b₂,b₃ // b₄,b₅ & b₂,b₃ // b₅,b₄ )

proof end;

theorem Th7: :: AFF_4:7

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆, b₇ being Subset of b₁ st ( b₆ // b₇ or b₇ // b₆ ) & b₂ <> b₃ & ( b₂,b₃ // b₄,b₅ or b₄,b₅ // b₂,b₃ ) & b₂ in b₆ & b₃ in b₆ & b₄ in b₇ holds
b₅ in b₇

proof end;

Lemma7: for b₁ being AffinSpace
for b₂, b₃, b₄ being Element of b₁
for b₅, b₆ being Subset of b₁ st b₅ // b₆ & b₂ in b₅ & b₃ in b₅ & b₄ in b₆ holds
ex b₇ being Element of b₁ st
( b₇ in b₆ & b₂,b₄ // b₃,b₇ )

proof end;

theorem Th8: :: AFF_4:8

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁
for b₇, b₈ being Subset of b₁ st b₂ in b₇ & b₂ in b₈ & b₃ in b₇ & b₄ in b₇ & b₅ in b₈ & b₆ in b₈ & b₂ <> b₃ & b₂ <> b₅ & b₇ <> b₈ & ( b₃,b₅ // b₄,b₆ or b₅,b₃ // b₆,b₄ ) & b₇ is_line & b₈ is_line & b₂ = b₄ holds
b₂ = b₆

proof end;

theorem Th9: :: AFF_4:9

proof end;

theorem Th10: :: AFF_4:10

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆, b₇ being Subset of b₁ st ( b₆ // b₇ or b₇ // b₆ ) & b₂ in b₆ & b₃ in b₆ & b₄ in b₇ & b₅ in b₇ & b₆ <> b₇ & ( b₂,b₄ // b₃,b₅ or b₄,b₂ // b₅,b₃ ) & b₂ = b₃ holds
b₄ = b₅

proof end;

theorem Th11: :: AFF_4:11

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁ ex b₄ being Subset of b₁ st
( b₂ in b₄ & b₃ in b₄ & b₄ is_line )

proof end;

theorem Th12: :: AFF_4:12

for b₁ being AffinSpace
for b₂ being Subset of b₁ st b₂ is_line holds
ex b₃ being Element of b₁ st not b₃ in b₂

proof end;

definition

let c₁ be AffinSpace;
let c₂, c₃ be Subset of c₁;
func Plane c₂,c₃ -> Subset of a₁ equals :: AFF_4:def 1
{ b₁ where B is Element of a₁ : ex b₁ being Element of a₁ st
( b₁,b₂ // a₂ & b₂ in a₃ ) } ;
coherence

proof end;

end;

:: deftheorem Def1 defines Plane AFF_4:def 1 :

definition

let c₁ be AffinSpace;
let c₂ be Subset of c₁;
attr a₂ is being_plane means :Def2: :: AFF_4:def 2
ex b₁, b₂ being Subset of a₁ st
( b₁ is_line & b₂ is_line & not b₁ // b₂ & a₂ = Plane b₁,b₂ );

end;

:: deftheorem Def2 defines being_plane AFF_4:def 2 :

notation

let c₁ be AffinSpace;
let c₂ be Subset of c₁;
synonym c₂ is_plane for being_plane c₂;

end;

Lemma14: for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁
for b₄ being Element of b₁ holds
( b₄ in Plane b₂,b₃ iff ex b₅ being Element of b₁ st
( b₄,b₅ // b₂ & b₅ in b₃ ) )

proof end;

theorem Th13: :: AFF_4:13

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁ st not b₂ is_line holds
Plane b₂,b₃ = {}

proof end;

theorem Th14: :: AFF_4:14

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁ st b₂ is_line holds
b₃ c= Plane b₂,b₃

proof end;

theorem Th15: :: AFF_4:15

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁ st b₂ // b₃ holds
Plane b₂,b₃ = b₃

proof end;

theorem Th16: :: AFF_4:16

for b₁ being AffinSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ // b₃ holds
Plane b₂,b₄ = Plane b₃,b₄

proof end;

theorem Th17: :: AFF_4:17

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁
for b₇, b₈, b₉, b₁₀ being Subset of b₁ st b₂ in b₇ & b₃ in b₇ & b₄ in b₇ & b₂ in b₈ & b₅ in b₈ & b₆ in b₈ & not b₂ in b₉ & not b₂ in b₁₀ & b₇ <> b₈ & b₃ in b₉ & b₅ in b₉ & b₄ in b₁₀ & b₆ in b₁₀ & b₇ is_line & b₈ is_line & b₉ is_line & b₁₀ is_line & not b₉ // b₁₀ holds
ex b₁₁ being Element of b₁ st
( b₁₁ in b₉ & b₁₁ in b₁₀ )

proof end;

theorem Th18: :: AFF_4:18

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆, b₇, b₈, b₉ being Subset of b₁ st b₂ in b₆ & b₃ in b₆ & b₄ in b₇ & b₅ in b₇ & b₂ in b₈ & b₄ in b₈ & b₃ in b₉ & b₅ in b₉ & b₆ <> b₇ & b₆ // b₇ & b₈ is_line & b₉ is_line & not b₈ // b₉ holds
ex b₁₀ being Element of b₁ st
( b₁₀ in b₈ & b₁₀ in b₉ )

proof end;

Lemma18: for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃, b₄, b₅ being Subset of b₁ st b₃ is_line & b₄ is_line & b₂ in b₅ & b₂ in Plane b₃,b₄ & b₃ // b₅ holds
b₅ c= Plane b₃,b₄

proof end;

Lemma19: for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄, b₅, b₆ being Subset of b₁ st b₄ is_line & b₅ is_line & b₆ is_line & b₂ in Plane b₄,b₅ & b₃ in Plane b₄,b₅ & b₂ <> b₃ & b₂ in b₆ & b₃ in b₆ holds
b₆ c= Plane b₄,b₅

proof end;

theorem Th19: :: AFF_4:19

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ st b₄ is_plane & b₂ in b₄ & b₃ in b₄ & b₂ <> b₃ holds
Line b₂,b₃ c= b₄

proof end;

Lemma21: for b₁ being AffinSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ is_line & b₃ is_line & b₄ is_line & b₄ c= Plane b₂,b₃ holds
Plane b₂,b₄ c= Plane b₂,b₃

proof end;

theorem Th20: :: AFF_4:20

for b₁ being AffinSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ is_line & b₃ is_line & b₄ is_line & not b₂ // b₃ & not b₂ // b₄ & b₄ c= Plane b₂,b₃ holds
Plane b₂,b₄ = Plane b₂,b₃

proof end;

theorem Th21: :: AFF_4:21

for b₁ being AffinSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ is_line & b₃ is_line & b₄ is_line & b₄ c= Plane b₂,b₃ & not b₃ // b₄ holds
ex b₅ being Element of b₁ st
( b₅ in b₃ & b₅ in b₄ )

proof end;

theorem Th22: :: AFF_4:22

for b₁ being AffinSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ is_plane & b₃ is_line & b₄ is_line & b₃ c= b₂ & b₄ c= b₂ & not b₃ // b₄ holds
ex b₅ being Element of b₁ st
( b₅ in b₃ & b₅ in b₄ )

proof end;

theorem Th23: :: AFF_4:23

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃, b₄, b₅ being Subset of b₁ st b₃ is_plane & b₂ in b₃ & b₄ c= b₃ & b₂ in b₅ & ( b₄ // b₅ or b₅ // b₄ ) holds
b₅ c= b₃

proof end;

theorem Th24: :: AFF_4:24

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄, b₅ being Subset of b₁ st b₄ is_plane & b₅ is_plane & b₂ in b₄ & b₃ in b₄ & b₂ in b₅ & b₃ in b₅ & b₄ <> b₅ & b₂ <> b₃ holds
b₄ /\ b₅ is_line

proof end;

theorem Th25: :: AFF_4:25

for b₁ being AffinSpace
for b₂, b₃, b₄ being Element of b₁
for b₅, b₆ being Subset of b₁ st b₅ is_plane & b₆ is_plane & b₂ in b₅ & b₃ in b₅ & b₄ in b₅ & b₂ in b₆ & b₃ in b₆ & b₄ in b₆ & not LIN b₂,b₃,b₄ holds
b₅ = b₆

proof end;

Lemma28: for b₁ being AffinSpace
for b₂, b₃, b₄ being Element of b₁
for b₅ being Subset of b₁ st b₅ is_line & b₂ in b₅ & b₃ in b₅ & b₂ <> b₃ & not b₄ in b₅ holds
not LIN b₂,b₃,b₄

proof end;

theorem Th26: :: AFF_4:26

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂ is_plane & b₃ is_plane & b₄ is_line & b₅ is_line & b₄ c= b₂ & b₅ c= b₂ & b₄ c= b₃ & b₅ c= b₃ & b₄ <> b₅ holds
b₂ = b₃

proof end;

definition

let c₁ be AffinSpace;
let c₂ be Element of c₁;
let c₃ be Subset of c₁;
assume E30: c₃ is_line ;
func c₂ * c₃ -> Subset of a₁ means :Def3: :: AFF_4:def 3
( a₂ in a₄ & a₃ // a₄ );
existence by E30, AFF_1:63;
uniqueness by AFF_1:64;

end;

:: deftheorem Def3 defines * AFF_4:def 3 :

theorem Th27: :: AFF_4:27

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₃ is_line holds
b₂ * b₃ is_line

proof end;

theorem Th28: :: AFF_4:28

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃, b₄ being Subset of b₁ st b₃ is_plane & b₄ is_line & b₂ in b₃ & b₄ c= b₃ holds
b₂ * b₄ c= b₃

proof end;

theorem Th29: :: AFF_4:29

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆ being Subset of b₁ st b₆ is_plane & b₂ in b₆ & b₃ in b₆ & b₄ in b₆ & b₂,b₃ // b₄,b₅ & b₂ <> b₃ holds
b₅ in b₆

proof end;

theorem Th30: :: AFF_4:30

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₃ is_line holds
( b₂ in b₃ iff b₂ * b₃ = b₃ )

proof end;

theorem Th31: :: AFF_4:31

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ st b₄ is_line holds
b₂ * b₄ = b₂ * (b₃ * b₄)

proof end;

Lemma35: for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₃ is_line & b₂ in b₃ holds
b₂ * b₃ = b₃

proof end;

theorem Th32: :: AFF_4:32

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃, b₄ being Subset of b₁ st b₃ // b₄ holds
b₂ * b₃ = b₂ * b₄

proof end;

definition

let c₁ be AffinSpace;
let c₂, c₃ be Subset of c₁;
pred c₂ '||' c₃ means :Def4: :: AFF_4:def 4
for b₁ being Element of a₁
for b₂ being Subset of a₁ st b₁ in a₃ & b₂ is_line & b₂ c= a₂ holds
b₁ * b₂ c= a₃;

end;

:: deftheorem Def4 defines '||' AFF_4:def 4 :

theorem Th33: :: AFF_4:33

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ & ( ( b₂ is_line & b₃ is_line ) or ( b₂ is_plane & b₃ is_plane ) ) holds
b₂ = b₃

proof end;

theorem Th34: :: AFF_4:34

for b₁ being AffinSpace
for b₂ being Subset of b₁ st b₂ is_plane holds
ex b₃, b₄, b₅ being Element of b₁ st
( b₃ in b₂ & b₄ in b₂ & b₅ in b₂ & not LIN b₃,b₄,b₅ )

proof end;

Lemma40: for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₃ is_plane holds
ex b₄, b₅ being Element of b₁ st
( b₄ in b₃ & b₅ in b₃ & not LIN b₂,b₄,b₅ )

proof end;

theorem Th35: :: AFF_4:35

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁ st b₂ is_line & b₃ is_plane holds
ex b₄ being Element of b₁ st
( b₄ in b₃ & not b₄ in b₂ )

proof end;

theorem Th36: :: AFF_4:36

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₃ is_line holds
ex b₄ being Subset of b₁ st
( b₂ in b₄ & b₃ c= b₄ & b₄ is_plane )

proof end;

theorem Th37: :: AFF_4:37

for b₁ being AffinSpace
for b₂, b₃, b₄ being Element of b₁ ex b₅ being Subset of b₁ st
( b₂ in b₅ & b₃ in b₅ & b₄ in b₅ & b₅ is_plane )

proof end;

theorem Th38: :: AFF_4:38

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃, b₄ being Subset of b₁ st b₂ in b₃ & b₂ in b₄ & b₃ is_line & b₄ is_line holds
ex b₅ being Subset of b₁ st
( b₃ c= b₅ & b₄ c= b₅ & b₅ is_plane )

proof end;

theorem Th39: :: AFF_4:39

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁ st b₂ // b₃ holds
ex b₄ being Subset of b₁ st
( b₂ c= b₄ & b₃ c= b₄ & b₄ is_plane )

proof end;

theorem Th40: :: AFF_4:40

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁ st b₂ is_line & b₃ is_line holds
( b₂ // b₃ iff b₂ '||' b₃ )

proof end;

theorem Th41: :: AFF_4:41

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁ st b₂ is_line & b₃ is_plane holds
( b₂ '||' b₃ iff ex b₄ being Subset of b₁ st
( b₄ c= b₃ & ( b₂ // b₄ or b₄ // b₂ ) ) )

proof end;

theorem Th42: :: AFF_4:42

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁ st b₂ is_line & b₃ is_plane & b₂ c= b₃ holds
b₂ '||' b₃

proof end;

theorem Th43: :: AFF_4:43

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃, b₄ being Subset of b₁ st b₃ is_line & b₄ is_plane & b₂ in b₃ & b₂ in b₄ & b₃ '||' b₄ holds
b₃ c= b₄

proof end;

definition

let c₁ be AffinSpace;
let c₂, c₃, c₄ be Subset of c₁;
pred c₂,c₃,c₄ is_coplanar means :Def5: :: AFF_4:def 5
ex b₁ being Subset of a₁ st
( a₂ c= b₁ & a₃ c= b₁ & a₄ c= b₁ & b₁ is_plane );

end;

:: deftheorem Def5 defines is_coplanar AFF_4:def 5 :

theorem Th44: :: AFF_4:44

for b₁ being AffinSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂,b₃,b₄ is_coplanar holds
( b₂,b₄,b₃ is_coplanar & b₃,b₂,b₄ is_coplanar & b₃,b₄,b₂ is_coplanar & b₄,b₂,b₃ is_coplanar & b₄,b₃,b₂ is_coplanar )

proof end;

theorem Th45: :: AFF_4:45

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂ is_line & b₃ is_line & b₄ is_line & b₅ is_line & b₄,b₅,b₃ is_coplanar & b₄,b₅,b₂ is_coplanar & b₄ <> b₅ holds
b₄,b₃,b₂ is_coplanar

proof end;

theorem Th46: :: AFF_4:46

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂ is_line & b₃ is_line & b₄ is_plane & b₂ c= b₄ & b₃ c= b₄ & b₂ <> b₃ holds
( b₂,b₃,b₅ is_coplanar iff b₅ c= b₄ )

proof end;

theorem Th47: :: AFF_4:47

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃, b₄ being Subset of b₁ st b₂ in b₃ & b₂ in b₄ & b₃ is_line & b₄ is_line holds
( b₃,b₄,b₄ is_coplanar & b₄,b₃,b₄ is_coplanar & b₄,b₄,b₃ is_coplanar )

proof end;

theorem Th48: :: AFF_4:48

for b₁ being AffinSpace
for b₂ being Subset of b₁ st b₁ is not AffinPlane & b₂ is_plane holds
ex b₃ being Element of b₁ st not b₃ in b₂

proof end;

Lemma51: for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁
for b₉, b₁₀, b₁₁ being Subset of b₁ st b₂ in b₉ & b₂ in b₁₀ & b₂ in b₁₁ & not b₉,b₁₀,b₁₁ is_coplanar & b₂ <> b₃ & b₂ <> b₄ & b₂ <> b₅ & b₃ in b₉ & b₆ in b₉ & b₄ in b₁₀ & b₇ in b₁₀ & b₅ in b₁₁ & b₈ in b₁₁ & b₉ is_line & b₁₀ is_line & b₁₁ is_line & b₉ <> b₁₀ & b₉ <> b₁₁ & b₃,b₄ // b₆,b₇ & b₃,b₅ // b₆,b₈ holds
b₄,b₅ // b₇,b₈

proof end;

theorem Th49: :: AFF_4:49

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁
for b₉, b₁₀, b₁₁ being Subset of b₁ st b₁ is not AffinPlane & b₂ in b₉ & b₂ in b₁₀ & b₂ in b₁₁ & b₂ <> b₃ & b₂ <> b₄ & b₂ <> b₅ & b₃ in b₉ & b₆ in b₉ & b₄ in b₁₀ & b₇ in b₁₀ & b₅ in b₁₁ & b₈ in b₁₁ & b₉ is_line & b₁₀ is_line & b₁₁ is_line & b₉ <> b₁₀ & b₉ <> b₁₁ & b₃,b₄ // b₆,b₇ & b₃,b₅ // b₆,b₈ holds
b₄,b₅ // b₇,b₈

proof end;

theorem Th50: :: AFF_4:50

for b₁ being AffinSpace st b₁ is not AffinPlane holds
b₁ is Desarguesian

proof end;

Lemma53: for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁
for b₈, b₉, b₁₀ being Subset of b₁ st b₈ // b₉ & b₈ // b₁₀ & not b₈,b₉,b₁₀ is_coplanar & b₂ in b₈ & b₃ in b₈ & b₄ in b₉ & b₅ in b₉ & b₆ in b₁₀ & b₇ in b₁₀ & b₈ is_line & b₉ is_line & b₁₀ is_line & b₈ <> b₉ & b₈ <> b₁₀ & b₂,b₄ // b₃,b₅ & b₂,b₆ // b₃,b₇ holds
b₄,b₆ // b₅,b₇

proof end;

theorem Th51: :: AFF_4:51

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁
for b₈, b₉, b₁₀ being Subset of b₁ st b₁ is not AffinPlane & b₈ // b₉ & b₈ // b₁₀ & b₂ in b₈ & b₃ in b₈ & b₄ in b₉ & b₅ in b₉ & b₆ in b₁₀ & b₇ in b₁₀ & b₈ is_line & b₉ is_line & b₁₀ is_line & b₈ <> b₉ & b₈ <> b₁₀ & b₂,b₄ // b₃,b₅ & b₂,b₆ // b₃,b₇ holds
b₄,b₆ // b₅,b₇

proof end;

theorem Th52: :: AFF_4:52

for b₁ being AffinSpace st b₁ is not AffinPlane holds
b₁ is translational

proof end;

theorem Th53: :: AFF_4:53

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₁ is AffinPlane & not LIN b₂,b₃,b₄ holds
ex b₇ being Element of b₁ st
( b₂,b₄ // b₅,b₇ & b₃,b₄ // b₆,b₇ )

proof end;

Lemma56: for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁
for b₇ being Subset of b₁ st not LIN b₂,b₃,b₄ & b₅ <> b₆ & b₂,b₃ // b₅,b₆ & b₂ in b₇ & b₃ in b₇ & b₄ in b₇ & b₇ is_plane & b₅ in b₇ holds
ex b₈ being Element of b₁ st
( b₂,b₄ // b₅,b₈ & b₃,b₄ // b₆,b₈ )

proof end;

theorem Th54: :: AFF_4:54

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not LIN b₂,b₃,b₄ & b₅ <> b₆ & b₂,b₃ // b₅,b₆ holds
ex b₇ being Element of b₁ st
( b₂,b₄ // b₅,b₇ & b₃,b₄ // b₆,b₇ )

proof end;

theorem Th55: :: AFF_4:55

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁ st b₂ is_plane & b₃ is_plane holds
( b₂ '||' b₃ iff ex b₄, b₅, b₆, b₇ being Subset of b₁ st
( not b₄ // b₅ & b₄ c= b₂ & b₅ c= b₂ & b₆ c= b₃ & b₇ c= b₃ & ( b₄ // b₆ or b₆ // b₄ ) & ( b₅ // b₇ or b₇ // b₅ ) ) )

proof end;

theorem Th56: :: AFF_4:56

for b₁ being AffinSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ // b₃ & b₃ '||' b₄ holds
b₂ '||' b₄

proof end;

theorem Th57: :: AFF_4:57

for b₁ being AffinSpace
for b₂ being Subset of b₁ st b₂ is_plane holds
b₂ '||' b₂

proof end;

theorem Th58: :: AFF_4:58

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁ st b₂ is_plane & b₃ is_plane & b₂ '||' b₃ holds
b₃ '||' b₂

proof end;

theorem Th59: :: AFF_4:59

for b₁ being AffinSpace
for b₂ being Subset of b₁ st b₂ is_plane holds
b₂ <> {}

proof end;

theorem Th60: :: AFF_4:60

for b₁ being AffinSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ '||' b₃ & b₃ '||' b₄ & b₃ <> {} holds
b₂ '||' b₄

proof end;

Lemma63: for b₁ being AffinSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ is_plane & b₃ is_plane & b₄ is_plane & b₂ '||' b₃ & b₃ '||' b₄ holds
b₂ '||' b₄

proof end;

theorem Th61: :: AFF_4:61

for b₁ being AffinSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ is_plane & b₃ is_plane & b₄ is_plane & ( ( b₂ '||' b₃ & b₃ '||' b₄ ) or ( b₂ '||' b₃ & b₄ '||' b₃ ) or ( b₃ '||' b₂ & b₃ '||' b₄ ) or ( b₃ '||' b₂ & b₄ '||' b₃ ) ) holds
( b₂ '||' b₄ & b₄ '||' b₂ )

proof end;

Lemma65: for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁ st b₂ is_plane & b₃ is_plane & b₂ '||' b₃ & b₂ <> b₃ holds
for b₄ being Element of b₁ holds
( not b₄ in b₂ or not b₄ in b₃ )

proof end;

theorem Th62: :: AFF_4:62

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃, b₄ being Subset of b₁ st b₃ is_plane & b₄ is_plane & b₂ in b₃ & b₂ in b₄ & b₃ '||' b₄ holds
b₃ = b₄ by Lemma65;

theorem Th63: :: AFF_4:63

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆, b₇, b₈ being Subset of b₁ st b₆ is_plane & b₇ is_plane & b₈ is_plane & b₆ '||' b₇ & b₆ <> b₇ & b₂ in b₆ /\ b₈ & b₃ in b₆ /\ b₈ & b₄ in b₇ /\ b₈ & b₅ in b₇ /\ b₈ holds
b₂,b₃ // b₄,b₅

proof end;

theorem Th64: :: AFF_4:64

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆, b₇, b₈ being Subset of b₁ st b₆ is_plane & b₇ is_plane & b₈ is_plane & b₆ '||' b₇ & b₂ in b₆ /\ b₈ & b₃ in b₆ /\ b₈ & b₄ in b₇ /\ b₈ & b₅ in b₇ /\ b₈ & b₆ <> b₇ & b₂ <> b₃ & b₄ <> b₅ holds
b₆ /\ b₈ // b₇ /\ b₈

proof end;

theorem Th65: :: AFF_4:65

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₃ is_plane holds
ex b₄ being Subset of b₁ st
( b₂ in b₄ & b₃ '||' b₄ & b₄ is_plane )

proof end;

definition

let c₁ be AffinSpace;
let c₂ be Element of c₁;
let c₃ be Subset of c₁;
assume E68: c₃ is_plane ;
func c₂ + c₃ -> Subset of a₁ means :Def6: :: AFF_4:def 6
( a₂ in a₄ & a₃ '||' a₄ & a₄ is_plane );
existence by E68, Th65;
uniqueness

proof end;

end;

:: deftheorem Def6 defines + AFF_4:def 6 :

theorem Th66: :: AFF_4:66

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₃ is_plane holds
( b₂ in b₃ iff b₂ + b₃ = b₃ )

proof end;

theorem Th67: :: AFF_4:67

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ st b₄ is_plane holds
b₂ + b₄ = b₂ + (b₃ + b₄)

proof end;

theorem Th68: :: AFF_4:68

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃, b₄ being Subset of b₁ st b₃ is_line & b₄ is_plane & b₃ '||' b₄ holds
b₂ * b₃ c= b₂ + b₄

proof end;

theorem Th69: :: AFF_4:69

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃, b₄ being Subset of b₁ st b₃ is_plane & b₄ is_plane & b₃ '||' b₄ holds
b₂ + b₃ = b₂ + b₄

proof end;