:: AFPROJ semantic presentation

theorem Th1: :: AFPROJ:1

for b₁ being AffinSpace
for b₂ being Subset of b₁ st b₁ is AffinPlane & b₂ = the carrier of b₁ holds
b₂ is_plane

proof end;

theorem Th2: :: AFPROJ:2

for b₁ being AffinSpace
for b₂ being Subset of b₁ st b₁ is AffinPlane & b₂ is_plane holds
b₂ = the carrier of b₁

proof end;

theorem Th3: :: AFPROJ:3

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁ st b₁ is AffinPlane & b₂ is_plane & b₃ is_plane holds
b₂ = b₃

proof end;

theorem Th4: :: AFPROJ:4

for b₁ being AffinSpace
for b₂ being Subset of b₁ st b₂ = the carrier of b₁ & b₂ is_plane holds
b₁ is AffinPlane

proof end;

theorem Th5: :: AFPROJ:5

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

proof end;

theorem Th6: :: AFPROJ:6

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

proof end;

definition

let c₁ be AffinSpace;
func AfLines c₁ -> Subset-Family of a₁ equals :: AFPROJ:def 1
{ b₁ where B is Subset of a₁ : b₁ is_line } ;
coherence

proof end;

end;

:: deftheorem Def1 defines AfLines AFPROJ:def 1 :

definition

let c₁ be AffinSpace;
func AfPlanes c₁ -> Subset-Family of a₁ equals :: AFPROJ:def 2
{ b₁ where B is Subset of a₁ : b₁ is_plane } ;
coherence

proof end;

end;

:: deftheorem Def2 defines AfPlanes AFPROJ:def 2 :

theorem Th7: :: AFPROJ:7

for b₁ being AffinSpace
for b₂ being set holds
( b₂ in AfLines b₁ iff ex b₃ being Subset of b₁ st
( b₂ = b₃ & b₃ is_line ) ) ;

theorem Th8: :: AFPROJ:8

for b₁ being AffinSpace
for b₂ being set holds
( b₂ in AfPlanes b₁ iff ex b₃ being Subset of b₁ st
( b₂ = b₃ & b₃ is_plane ) ) ;

definition

let c₁ be AffinSpace;
func LinesParallelity c₁ -> Equivalence_Relation of AfLines a₁ equals :: AFPROJ:def 3
{ [b₁,b₂] where B is Subset of a₁, B is Subset of a₁ : ( b₁ is_line & b₂ is_line & b₁ '||' b₂ ) } ;
coherence

proof end;

end;

:: deftheorem Def3 defines LinesParallelity AFPROJ:def 3 :

definition

let c₁ be AffinSpace;
func PlanesParallelity c₁ -> Equivalence_Relation of AfPlanes a₁ equals :: AFPROJ:def 4
{ [b₁,b₂] where B is Subset of a₁, B is Subset of a₁ : ( b₁ is_plane & b₂ is_plane & b₁ '||' b₂ ) } ;
coherence

proof end;

end;

:: deftheorem Def4 defines PlanesParallelity AFPROJ:def 4 :

definition

let c₁ be AffinSpace;
let c₂ be Subset of c₁;
assume c₂ is_line ;
func LDir c₂ -> Subset of (AfLines a₁) equals :Def5: :: AFPROJ:def 5
Class (LinesParallelity a₁),a₂;
correctness ;

end;

:: deftheorem Def5 defines LDir AFPROJ:def 5 :

definition

let c₁ be AffinSpace;
let c₂ be Subset of c₁;
assume c₂ is_plane ;
func PDir c₂ -> Subset of (AfPlanes a₁) equals :Def6: :: AFPROJ:def 6
Class (PlanesParallelity a₁),a₂;
correctness ;

end;

:: deftheorem Def6 defines PDir AFPROJ:def 6 :

theorem Th9: :: AFPROJ:9

for b₁ being AffinSpace
for b₂ being Subset of b₁ st b₂ is_line holds
for b₃ being set holds
( b₃ in LDir b₂ iff ex b₄ being Subset of b₁ st
( b₃ = b₄ & b₄ is_line & b₂ '||' b₄ ) )

proof end;

theorem Th10: :: AFPROJ:10

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

proof end;

theorem Th11: :: AFPROJ:11

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

proof end;

theorem Th12: :: AFPROJ:12

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

proof end;

theorem Th13: :: AFPROJ:13

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁ st b₂ is_plane & b₃ is_plane holds
( PDir b₂ = PDir b₃ iff b₂ '||' b₃ )

proof end;

definition

let c₁ be AffinSpace;
func Dir_of_Lines c₁ -> non empty set equals :: AFPROJ:def 7
Class (LinesParallelity a₁);
coherence

proof end;

end;

:: deftheorem Def7 defines Dir_of_Lines AFPROJ:def 7 :

definition

let c₁ be AffinSpace;
func Dir_of_Planes c₁ -> non empty set equals :: AFPROJ:def 8
Class (PlanesParallelity a₁);
coherence

proof end;

end;

:: deftheorem Def8 defines Dir_of_Planes AFPROJ:def 8 :

theorem Th14: :: AFPROJ:14

for b₁ being AffinSpace
for b₂ being set holds
( b₂ in Dir_of_Lines b₁ iff ex b₃ being Subset of b₁ st
( b₂ = LDir b₃ & b₃ is_line ) )

proof end;

theorem Th15: :: AFPROJ:15

for b₁ being AffinSpace
for b₂ being set holds
( b₂ in Dir_of_Planes b₁ iff ex b₃ being Subset of b₁ st
( b₂ = PDir b₃ & b₃ is_plane ) )

proof end;

theorem Th16: :: AFPROJ:16

for b₁ being AffinSpace holds the carrier of b₁ misses Dir_of_Lines b₁

proof end;

theorem Th17: :: AFPROJ:17

for b₁ being AffinSpace st b₁ is AffinPlane holds
AfLines b₁ misses Dir_of_Planes b₁

proof end;

theorem Th18: :: AFPROJ:18

for b₁ being AffinSpace
for b₂ being set holds
( b₂ in [:(AfLines b₁),{1}:] iff ex b₃ being Subset of b₁ st
( b₂ = [b₃,1] & b₃ is_line ) )

proof end;

theorem Th19: :: AFPROJ:19

for b₁ being AffinSpace
for b₂ being set holds
( b₂ in [:(Dir_of_Planes b₁),{2}:] iff ex b₃ being Subset of b₁ st
( b₂ = [(PDir b₃),2] & b₃ is_plane ) )

proof end;

definition

let c₁ be AffinSpace;
func ProjectivePoints c₁ -> non empty set equals :: AFPROJ:def 9
the carrier of a₁ \/ (Dir_of_Lines a₁);
correctness ;

end;

:: deftheorem Def9 defines ProjectivePoints AFPROJ:def 9 :

definition

let c₁ be AffinSpace;
func ProjectiveLines c₁ -> non empty set equals :: AFPROJ:def 10
[:(AfLines a₁),{1}:] \/ [:(Dir_of_Planes a₁),{2}:];
coherence ;

end;

:: deftheorem Def10 defines ProjectiveLines AFPROJ:def 10 :

definition

let c₁ be AffinSpace;
func Proj_Inc c₁ -> Relation of ProjectivePoints a₁, ProjectiveLines a₁ means :Def11: :: AFPROJ:def 11
for b₁, b₂ being set holds
( [b₁,b₂] in a₂ iff ( ex b₃ being Subset of a₁ st
( b₃ is_line & b₂ = [b₃,1] & ( ( b₁ in the carrier of a₁ & b₁ in b₃ ) or b₁ = LDir b₃ ) ) or ex b₃, b₄ being Subset of a₁ st
( b₃ is_line & b₄ is_plane & b₁ = LDir b₃ & b₂ = [(PDir b₄),2] & b₃ '||' b₄ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines Proj_Inc AFPROJ:def 11 :

definition

let c₁ be AffinSpace;
func Inc_of_Dir c₁ -> Relation of Dir_of_Lines a₁, Dir_of_Planes a₁ means :Def12: :: AFPROJ:def 12
for b₁, b₂ being set holds
( [b₁,b₂] in a₂ iff ex b₃, b₄ being Subset of a₁ st
( b₁ = LDir b₃ & b₂ = PDir b₄ & b₃ is_line & b₄ is_plane & b₃ '||' b₄ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines Inc_of_Dir AFPROJ:def 12 :

definition

let c₁ be AffinSpace;
func IncProjSp_of c₁ -> strict IncProjStr equals :: AFPROJ:def 13
IncProjStr(# (ProjectivePoints a₁),(ProjectiveLines a₁),(Proj_Inc a₁) #);
correctness ;

end;

:: deftheorem Def13 defines IncProjSp_of AFPROJ:def 13 :

definition

let c₁ be AffinSpace;
func ProjHorizon c₁ -> strict IncProjStr equals :: AFPROJ:def 14
IncProjStr(# (Dir_of_Lines a₁),(Dir_of_Planes a₁),(Inc_of_Dir a₁) #);
correctness ;

end;

:: deftheorem Def14 defines ProjHorizon AFPROJ:def 14 :

theorem Th20: :: AFPROJ:20

for b₁ being AffinSpace
for b₂ being set holds
( b₂ is POINT of (IncProjSp_of b₁) iff ( b₂ is Element of b₁ or ex b₃ being Subset of b₁ st
( b₂ = LDir b₃ & b₃ is_line ) ) )

proof end;

theorem Th21: :: AFPROJ:21

for b₁ being AffinSpace
for b₂ being set holds
( b₂ is Element of the Points of (ProjHorizon b₁) iff ex b₃ being Subset of b₁ st
( b₂ = LDir b₃ & b₃ is_line ) ) by Th14;

theorem Th22: :: AFPROJ:22

for b₁ being AffinSpace
for b₂ being set st b₂ is Element of the Points of (ProjHorizon b₁) holds
b₂ is POINT of (IncProjSp_of b₁)

proof end;

theorem Th23: :: AFPROJ:23

for b₁ being AffinSpace
for b₂ being set holds
( b₂ is LINE of (IncProjSp_of b₁) iff ex b₃ being Subset of b₁ st
( ( b₂ = [b₃,1] & b₃ is_line ) or ( b₂ = [(PDir b₃),2] & b₃ is_plane ) ) )

proof end;

theorem Th24: :: AFPROJ:24

for b₁ being AffinSpace
for b₂ being set holds
( b₂ is Element of the Lines of (ProjHorizon b₁) iff ex b₃ being Subset of b₁ st
( b₂ = PDir b₃ & b₃ is_plane ) ) by Th15;

theorem Th25: :: AFPROJ:25

for b₁ being AffinSpace
for b₂ being set st b₂ is Element of the Lines of (ProjHorizon b₁) holds
[b₂,2] is LINE of (IncProjSp_of b₁)

proof end;

theorem Th26: :: AFPROJ:26

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃ being Subset of b₁
for b₄ being POINT of (IncProjSp_of b₁)
for b₅ being LINE of (IncProjSp_of b₁) st b₂ = b₄ & [b₃,1] = b₅ holds
( b₄ on b₅ iff ( b₃ is_line & b₂ in b₃ ) )

proof end;

theorem Th27: :: AFPROJ:27

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃ being Subset of b₁
for b₄ being POINT of (IncProjSp_of b₁)
for b₅ being LINE of (IncProjSp_of b₁) st b₂ = b₄ & [(PDir b₃),2] = b₅ & b₃ is_plane holds
not b₄ on b₅

proof end;

theorem Th28: :: AFPROJ:28

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁
for b₄ being POINT of (IncProjSp_of b₁)
for b₅ being LINE of (IncProjSp_of b₁) st b₄ = LDir b₂ & [b₃,1] = b₅ & b₂ is_line & b₃ is_line holds
( b₄ on b₅ iff b₂ '||' b₃ )

proof end;

theorem Th29: :: AFPROJ:29

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁
for b₄ being POINT of (IncProjSp_of b₁)
for b₅ being LINE of (IncProjSp_of b₁) st b₄ = LDir b₂ & b₅ = [(PDir b₃),2] & b₂ is_line & b₃ is_plane holds
( b₄ on b₅ iff b₂ '||' b₃ )

proof end;

theorem Th30: :: AFPROJ:30

for b₁ being AffinSpace
for b₂ being Subset of b₁
for b₃ being POINT of (IncProjSp_of b₁)
for b₄ being LINE of (IncProjSp_of b₁) st b₂ is_line & b₃ = LDir b₂ & b₄ = [b₂,1] holds
b₃ on b₄

proof end;

theorem Th31: :: AFPROJ:31

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁
for b₄ being POINT of (IncProjSp_of b₁)
for b₅ being LINE of (IncProjSp_of b₁) st b₂ is_line & b₃ is_plane & b₂ c= b₃ & b₄ = LDir b₂ & b₅ = [(PDir b₃),2] holds
b₄ on b₅

proof end;

theorem Th32: :: AFPROJ:32

for b₁ being AffinSpace
for b₂, b₃, b₄ being Subset of b₁
for b₅ being POINT of (IncProjSp_of b₁)
for b₆ being LINE of (IncProjSp_of b₁) st b₂ is_plane & b₃ c= b₂ & b₄ // b₃ & b₅ = LDir b₄ & b₆ = [(PDir b₂),2] holds
b₅ on b₆

proof end;

theorem Th33: :: AFPROJ:33

for b₁ being AffinSpace
for b₂ being Subset of b₁
for b₃ being POINT of (IncProjSp_of b₁)
for b₄ being LINE of (IncProjSp_of b₁) st b₄ = [(PDir b₂),2] & b₂ is_plane & b₃ on b₄ holds
not b₃ is Element of b₁ by Th27;

theorem Th34: :: AFPROJ:34

for b₁ being AffinSpace
for b₂ being Subset of b₁
for b₃ being POINT of (IncProjSp_of b₁)
for b₄ being LINE of (IncProjSp_of b₁) st b₄ = [b₂,1] & b₂ is_line & b₃ on b₄ & b₃ is not Element of b₁ holds
b₃ = LDir b₂

proof end;

theorem Th35: :: AFPROJ:35

for b₁ being AffinSpace
for b₂ being Subset of b₁
for b₃, b₄ being POINT of (IncProjSp_of b₁)
for b₅ being LINE of (IncProjSp_of b₁) st b₅ = [b₂,1] & b₂ is_line & b₃ on b₅ & b₄ on b₅ & b₄ <> b₃ & b₃ is not Element of the carrier of b₁ holds
b₄ is Element of b₁

proof end;

theorem Th36: :: AFPROJ:36

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁
for b₄ being Element of the Points of (ProjHorizon b₁)
for b₅ being Element of the Lines of (ProjHorizon b₁) st b₄ = LDir b₂ & b₅ = PDir b₃ & b₂ is_line & b₃ is_plane holds
( b₄ on b₅ iff b₂ '||' b₃ )

proof end;

theorem Th37: :: AFPROJ:37

for b₁ being AffinSpace
for b₂ being Element of the Points of (ProjHorizon b₁)
for b₃ being Element of the Points of (IncProjSp_of b₁)
for b₄ being Element of the Lines of (ProjHorizon b₁)
for b₅ being LINE of (IncProjSp_of b₁) st b₃ = b₂ & b₅ = [b₄,2] holds
( b₂ on b₄ iff b₃ on b₅ )

proof end;

theorem Th38: :: AFPROJ:38

for b₁ being AffinSpace
for b₂, b₃ being Element of the Points of (ProjHorizon b₁)
for b₄, b₅ being Element of the Lines of (ProjHorizon b₁) st b₂ on b₄ & b₂ on b₅ & b₃ on b₄ & b₃ on b₅ & not b₂ = b₃ holds
b₄ = b₅

proof end;

theorem Th39: :: AFPROJ:39

for b₁ being AffinSpace
for b₂ being Element of the Lines of (ProjHorizon b₁) ex b₃, b₄, b₅ being Element of the Points of (ProjHorizon b₁) st
( b₃ on b₂ & b₄ on b₂ & b₅ on b₂ & b₃ <> b₄ & b₄ <> b₅ & b₅ <> b₃ )

proof end;

theorem Th40: :: AFPROJ:40

for b₁ being AffinSpace
for b₂, b₃ being Element of the Points of (ProjHorizon b₁) ex b₄ being Element of the Lines of (ProjHorizon b₁) st
( b₂ on b₄ & b₃ on b₄ )

proof end;

Lemma42: for b₁ being AffinSpace st b₁ is not AffinPlane holds
ex b₂ being Element of the Points of (ProjHorizon b₁)ex b₃ being Element of the Lines of (ProjHorizon b₁) st not b₂ on b₃

proof end;

Lemma43: for b₁ being AffinSpace
for b₂, b₃ being POINT of (IncProjSp_of b₁)
for b₄, b₅ being LINE of (IncProjSp_of b₁) st b₂ on b₄ & b₂ on b₅ & b₃ on b₄ & b₃ on b₅ & not b₂ = b₃ holds
b₄ = b₅

proof end;

Lemma44: for b₁ being AffinSpace
for b₂ being LINE of (IncProjSp_of b₁) ex b₃, b₄, b₅ being POINT of (IncProjSp_of b₁) st
( b₃ on b₂ & b₄ on b₂ & b₅ on b₂ & b₃ <> b₄ & b₄ <> b₅ & b₅ <> b₃ )

proof end;

Lemma45: for b₁ being AffinSpace
for b₂, b₃ being POINT of (IncProjSp_of b₁) ex b₄ being LINE of (IncProjSp_of b₁) st
( b₂ on b₄ & b₃ on b₄ )

proof end;

Lemma46: for b₁ being AffinSpace
for b₂, b₃ being LINE of (IncProjSp_of b₁) st b₁ is AffinPlane holds
ex b₄ being POINT of (IncProjSp_of b₁) st
( b₄ on b₂ & b₄ on b₃ )

proof end;

Lemma47: for b₁ being AffinSpace holds
not for b₂ being POINT of (IncProjSp_of b₁)
for b₃ being LINE of (IncProjSp_of b₁) holds b₂ on b₃

proof end;

theorem Th41: :: AFPROJ:41

for b₁ being AffinSpace
for b₂, b₃ being Element of the Points of (ProjHorizon b₁)
for b₄ being Element of the Lines of (IncProjSp_of b₁) st b₂ <> b₃ & [b₂,b₄] in the Inc of (IncProjSp_of b₁) & [b₃,b₄] in the Inc of (IncProjSp_of b₁) holds
ex b₅ being Element of the Lines of (ProjHorizon b₁) st b₄ = [b₅,2]

proof end;

theorem Th42: :: AFPROJ:42

for b₁ being AffinSpace
for b₂ being POINT of (IncProjSp_of b₁)
for b₃ being Element of the Lines of (ProjHorizon b₁) st [b₂,[b₃,2]] in the Inc of (IncProjSp_of b₁) holds
b₂ is Element of the Points of (ProjHorizon b₁)

proof end;

Lemma50: for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃, b₄, b₅, b₆ being Subset of b₁
for b₇, b₈, b₉ being POINT of (IncProjSp_of b₁)
for b₁₀, b₁₁, b₁₂ being LINE of (IncProjSp_of b₁) st b₃ is_line & b₄ is_line & b₅ is_plane & b₃ c= b₅ & b₄ c= b₅ & b₂ = b₇ & b₁₀ = [b₃,1] & b₁₁ = [b₄,1] & b₁₀ <> b₁₁ & b₈ on b₁₀ & b₉ on b₁₁ & b₈ on b₁₂ & b₉ on b₁₂ & b₈ <> b₉ & b₁₂ = [b₆,1] & b₆ is_line holds
b₆ c= b₅

proof end;

Lemma51: for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃, b₄, b₅, b₆ being Subset of b₁
for b₇, b₈, b₉ being POINT of (IncProjSp_of b₁)
for b₁₀, b₁₁, b₁₂ being LINE of (IncProjSp_of b₁) st b₃ is_line & b₄ is_line & b₅ is_plane & b₃ c= b₅ & b₄ c= b₅ & b₂ = b₇ & b₁₀ = [b₃,1] & b₁₁ = [b₄,1] & b₁₀ <> b₁₁ & b₈ on b₁₀ & b₉ on b₁₁ & b₈ on b₁₂ & b₉ on b₁₂ & b₈ <> b₉ & b₁₂ = [(PDir b₆),2] & b₆ is_plane holds
( b₆ '||' b₅ & b₅ '||' b₆ )

proof end;

theorem Th43: :: AFPROJ:43

for b₁ being AffinSpace
for b₂, b₃, b₄ being Subset of b₁
for b₅, b₆ being LINE of (IncProjSp_of b₁) st b₂ is_plane & b₃ is_line & b₄ is_line & b₃ c= b₂ & b₄ c= b₂ & b₅ = [b₃,1] & b₆ = [b₄,1] holds
ex b₇ being POINT of (IncProjSp_of b₁) st
( b₇ on b₅ & b₇ on b₆ )

proof end;

Lemma53: for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆ being POINT of (IncProjSp_of b₁)
for b₇, b₈, b₉, b₁₀ being LINE of (IncProjSp_of b₁) st b₂ on b₇ & b₃ on b₇ & b₄ on b₈ & b₅ on b₈ & b₆ on b₇ & b₆ on b₈ & b₂ on b₉ & b₄ on b₉ & b₃ on b₁₀ & b₅ on b₁₀ & not b₆ on b₉ & not b₆ on b₁₀ & b₇ <> b₈ & b₆ is Element of b₁ holds
ex b₁₁ being POINT of (IncProjSp_of b₁) st
( b₁₁ on b₉ & b₁₁ on b₁₀ )

proof end;

Lemma54: for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆ being POINT of (IncProjSp_of b₁)
for b₇, b₈, b₉, b₁₀ being LINE of (IncProjSp_of b₁) st b₂ on b₇ & b₃ on b₇ & b₄ on b₈ & b₅ on b₈ & b₆ on b₇ & b₆ on b₈ & b₂ on b₉ & b₄ on b₉ & b₃ on b₁₀ & b₅ on b₁₀ & not b₆ on b₉ & not b₆ on b₁₀ & b₇ <> b₈ & b₆ is not Element of b₁ & b₂ is Element of b₁ holds
ex b₁₁ being POINT of (IncProjSp_of b₁) st
( b₁₁ on b₉ & b₁₁ on b₁₀ )

proof end;

Lemma55: for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆ being POINT of (IncProjSp_of b₁)
for b₇, b₈, b₉, b₁₀ being LINE of (IncProjSp_of b₁) st b₂ on b₇ & b₃ on b₇ & b₄ on b₈ & b₅ on b₈ & b₆ on b₇ & b₆ on b₈ & b₂ on b₉ & b₄ on b₉ & b₃ on b₁₀ & b₅ on b₁₀ & not b₆ on b₉ & not b₆ on b₁₀ & b₇ <> b₈ & b₆ is not Element of b₁ & ( b₂ is Element of b₁ or b₃ is Element of b₁ or b₄ is Element of b₁ or b₅ is Element of b₁ ) holds
ex b₁₁ being POINT of (IncProjSp_of b₁) st
( b₁₁ on b₉ & b₁₁ on b₁₀ )

proof end;

Lemma56: for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆ being POINT of (IncProjSp_of b₁)
for b₇, b₈, b₉, b₁₀ being LINE of (IncProjSp_of b₁) st b₂ on b₇ & b₃ on b₇ & b₄ on b₈ & b₅ on b₈ & b₆ on b₇ & b₆ on b₈ & b₂ on b₉ & b₄ on b₉ & b₃ on b₁₀ & b₅ on b₁₀ & not b₆ on b₉ & not b₆ on b₁₀ & b₇ <> b₈ holds
ex b₁₁ being POINT of (IncProjSp_of b₁) st
( b₁₁ on b₉ & b₁₁ on b₁₀ )

proof end;

theorem Th44: :: AFPROJ:44

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of the Points of (ProjHorizon b₁)
for b₇, b₈, b₉, b₁₀ being Element of the Lines of (ProjHorizon b₁) st b₂ on b₇ & b₃ on b₇ & b₄ on b₈ & b₅ on b₈ & b₆ on b₇ & b₆ on b₈ & b₂ on b₉ & b₄ on b₉ & b₃ on b₁₀ & b₅ on b₁₀ & not b₆ on b₉ & not b₆ on b₁₀ & b₇ <> b₈ holds
ex b₁₁ being Element of the Points of (ProjHorizon b₁) st
( b₁₁ on b₉ & b₁₁ on b₁₀ )

proof end;

registration

let c₁ be AffinSpace;
cluster IncProjSp_of a₁ -> strict partial linear up-2-dimensional up-3-rank Vebleian ;
correctness

proof end;

end;

registration

cluster strict 2-dimensional IncProjStr ;
existence

proof end;

end;

registration

let c₁ be AffinPlane;
cluster IncProjSp_of a₁ -> strict partial linear up-2-dimensional up-3-rank Vebleian 2-dimensional ;
correctness

proof end;

end;

theorem Th45: :: AFPROJ:45

for b₁ being AffinSpace st IncProjSp_of b₁ is 2-dimensional holds
b₁ is AffinPlane

proof end;

theorem Th46: :: AFPROJ:46

for b₁ being AffinSpace st b₁ is not AffinPlane holds
ProjHorizon b₁ is IncProjSp

proof end;

theorem Th47: :: AFPROJ:47

for b₁ being AffinSpace st ProjHorizon b₁ is IncProjSp holds
not b₁ is AffinPlane

proof end;

theorem Th48: :: AFPROJ:48

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁
for b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of the carrier of b₁ st b₂ is_line & b₃ is_line & b₂ <> b₃ & b₄ in b₂ & b₄ in b₃ & b₄ <> b₅ & b₄ <> b₈ & b₄ <> 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₅,b₉ // b₆,b₈ & b₆,b₁₀ // b₇,b₉ & ( b₅ = b₆ or b₆ = b₇ or b₅ = b₇ ) holds
b₅,b₁₀ // b₇,b₈

proof end;

theorem Th49: :: AFPROJ:49

for b₁ being AffinSpace st IncProjSp_of b₁ is Pappian holds
b₁ is Pappian

proof end;

theorem Th50: :: AFPROJ:50

for b₁ being AffinSpace
for b₂, b₃, b₄ being Subset of b₁
for b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being Element of the carrier of b₁ st 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₁₁ & ( b₅ = b₉ or b₆ = b₉ ) holds
b₇,b₈ // b₁₀,b₁₁

proof end;

theorem Th51: :: AFPROJ:51

for b₁ being AffinSpace st IncProjSp_of b₁ is Desarguesian holds
b₁ is Desarguesian

proof end;

theorem Th52: :: AFPROJ:52

for b₁ being AffinSpace st IncProjSp_of b₁ is Fanoian holds
b₁ is Fanoian

proof end;