:: A Projective Closure and Projective Horizon of an Affine Space :: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski :: :: Received December 17, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin :: The aim of this article is to formalize the well known construction of :: the projective closure of an affine space. We begin with some evident :: properties of planes in affine planes. theorem Th1: :: AFPROJ:1 for AS being AffinSpace for X being Subset of AS st AS is AffinPlane & X = the carrier of AS holds X is being_plane proofend; theorem Th2: :: AFPROJ:2 for AS being AffinSpace for X being Subset of AS st AS is AffinPlane & X is being_plane holds X = the carrier of AS proofend; theorem Th3: :: AFPROJ:3 for AS being AffinSpace for X, Y being Subset of AS st AS is AffinPlane & X is being_plane & Y is being_plane holds X = Y proofend; theorem :: AFPROJ:4 for AS being AffinSpace for X being Subset of AS st X = the carrier of AS & X is being_plane holds AS is AffinPlane proofend; theorem Th5: :: AFPROJ:5 for AS being AffinSpace for A, K, X, Y being Subset of AS st not A // K & A '||' X & A '||' Y & K '||' X & K '||' Y & A is being_line & K is being_line & X is being_plane & Y is being_plane holds X '||' Y proofend; theorem :: AFPROJ:6 for AS being AffinSpace for X, A, Y being Subset of AS st X is being_plane & A '||' X & X '||' Y holds A '||' Y by AFF_4:59, AFF_4:60; :: Next we distinguish two sets, one consisting of the lines, the second :: consisting of the planes of a given affine space and we consider two :: equivalence relations defined on each of these sets; theses relations :: are in fact the relation of parallelity restricted to suitable area. :: Their equivalence classes are called directions (of lines and planes, :: respectively); they are intended to be considered as new objects which :: extend the given affine space to a projective space. definition let AS be AffinSpace; func AfLines AS -> Subset-Family of AS equals :: AFPROJ:def 1 { A where A is Subset of AS : A is being_line } ; coherence { A where A is Subset of AS : A is being_line } is Subset-Family of AS proofend; end; :: deftheorem defines AfLines AFPROJ:def_1_:_ for AS being AffinSpace holds AfLines AS = { A where A is Subset of AS : A is being_line } ; definition let AS be AffinSpace; func AfPlanes AS -> Subset-Family of AS equals :: AFPROJ:def 2 { A where A is Subset of AS : A is being_plane } ; coherence { A where A is Subset of AS : A is being_plane } is Subset-Family of AS proofend; end; :: deftheorem defines AfPlanes AFPROJ:def_2_:_ for AS being AffinSpace holds AfPlanes AS = { A where A is Subset of AS : A is being_plane } ; theorem :: AFPROJ:7 for AS being AffinSpace for x being set holds ( x in AfLines AS iff ex X being Subset of AS st ( x = X & X is being_line ) ) ; theorem :: AFPROJ:8 for AS being AffinSpace for x being set holds ( x in AfPlanes AS iff ex X being Subset of AS st ( x = X & X is being_plane ) ) ; definition let AS be AffinSpace; func LinesParallelity AS -> Equivalence_Relation of (AfLines AS) equals :: AFPROJ:def 3 { [K,M] where K, M is Subset of AS : ( K is being_line & M is being_line & K '||' M ) } ; coherence { [K,M] where K, M is Subset of AS : ( K is being_line & M is being_line & K '||' M ) } is Equivalence_Relation of (AfLines AS) proofend; end; :: deftheorem defines LinesParallelity AFPROJ:def_3_:_ for AS being AffinSpace holds LinesParallelity AS = { [K,M] where K, M is Subset of AS : ( K is being_line & M is being_line & K '||' M ) } ; definition let AS be AffinSpace; func PlanesParallelity AS -> Equivalence_Relation of (AfPlanes AS) equals :: AFPROJ:def 4 { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ; coherence { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } is Equivalence_Relation of (AfPlanes AS) proofend; end; :: deftheorem defines PlanesParallelity AFPROJ:def_4_:_ for AS being AffinSpace holds PlanesParallelity AS = { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ; definition let AS be AffinSpace; let X be Subset of AS; func LDir X -> Subset of (AfLines AS) equals :: AFPROJ:def 5 Class ((LinesParallelity AS),X); correctness coherence Class ((LinesParallelity AS),X) is Subset of (AfLines AS); ; end; :: deftheorem defines LDir AFPROJ:def_5_:_ for AS being AffinSpace for X being Subset of AS holds LDir X = Class ((LinesParallelity AS),X); definition let AS be AffinSpace; let X be Subset of AS; func PDir X -> Subset of (AfPlanes AS) equals :: AFPROJ:def 6 Class ((PlanesParallelity AS),X); correctness coherence Class ((PlanesParallelity AS),X) is Subset of (AfPlanes AS); ; end; :: deftheorem defines PDir AFPROJ:def_6_:_ for AS being AffinSpace for X being Subset of AS holds PDir X = Class ((PlanesParallelity AS),X); theorem Th9: :: AFPROJ:9 for AS being AffinSpace for X being Subset of AS st X is being_line holds for x being set holds ( x in LDir X iff ex Y being Subset of AS st ( x = Y & Y is being_line & X '||' Y ) ) proofend; theorem Th10: :: AFPROJ:10 for AS being AffinSpace for X being Subset of AS st X is being_plane holds for x being set holds ( x in PDir X iff ex Y being Subset of AS st ( x = Y & Y is being_plane & X '||' Y ) ) proofend; theorem Th11: :: AFPROJ:11 for AS being AffinSpace for X, Y being Subset of AS st X is being_line & Y is being_line holds ( LDir X = LDir Y iff X // Y ) proofend; theorem Th12: :: AFPROJ:12 for AS being AffinSpace for X, Y being Subset of AS st X is being_line & Y is being_line holds ( LDir X = LDir Y iff X '||' Y ) proofend; theorem Th13: :: AFPROJ:13 for AS being AffinSpace for X, Y being Subset of AS st X is being_plane & Y is being_plane holds ( PDir X = PDir Y iff X '||' Y ) proofend; definition let AS be AffinSpace; func Dir_of_Lines AS -> non empty set equals :: AFPROJ:def 7 Class (LinesParallelity AS); coherence Class (LinesParallelity AS) is non empty set proofend; end; :: deftheorem defines Dir_of_Lines AFPROJ:def_7_:_ for AS being AffinSpace holds Dir_of_Lines AS = Class (LinesParallelity AS); definition let AS be AffinSpace; func Dir_of_Planes AS -> non empty set equals :: AFPROJ:def 8 Class (PlanesParallelity AS); coherence Class (PlanesParallelity AS) is non empty set proofend; end; :: deftheorem defines Dir_of_Planes AFPROJ:def_8_:_ for AS being AffinSpace holds Dir_of_Planes AS = Class (PlanesParallelity AS); theorem Th14: :: AFPROJ:14 for AS being AffinSpace for x being set holds ( x in Dir_of_Lines AS iff ex X being Subset of AS st ( x = LDir X & X is being_line ) ) proofend; theorem Th15: :: AFPROJ:15 for AS being AffinSpace for x being set holds ( x in Dir_of_Planes AS iff ex X being Subset of AS st ( x = PDir X & X is being_plane ) ) proofend; :: The point is to guarantee that the classes of new objects consist of really :: new objects. Clearly the set of directions of lines and the set of affine :: points do not intersect. However we cannot claim, in general, that the set :: of affine lines and the set of directions of planes do not intersect; this :: is evidently true only in the case of affine planes. Therefore we have to :: modify (slightly) a construction of the set of lines of the projective :: closure of affine space, when compared with (naive) intuitions. theorem Th16: :: AFPROJ:16 for AS being AffinSpace holds the carrier of AS misses Dir_of_Lines AS proofend; theorem :: AFPROJ:17 for AS being AffinSpace st AS is AffinPlane holds AfLines AS misses Dir_of_Planes AS proofend; theorem Th18: :: AFPROJ:18 for AS being AffinSpace for x being set holds ( x in [:(AfLines AS),{1}:] iff ex X being Subset of AS st ( x = [X,1] & X is being_line ) ) proofend; theorem Th19: :: AFPROJ:19 for AS being AffinSpace for x being set holds ( x in [:(Dir_of_Planes AS),{2}:] iff ex X being Subset of AS st ( x = [(PDir X),2] & X is being_plane ) ) proofend; definition let AS be AffinSpace; func ProjectivePoints AS -> non empty set equals :: AFPROJ:def 9 the carrier of AS \/ (Dir_of_Lines AS); correctness coherence the carrier of AS \/ (Dir_of_Lines AS) is non empty set ; ; end; :: deftheorem defines ProjectivePoints AFPROJ:def_9_:_ for AS being AffinSpace holds ProjectivePoints AS = the carrier of AS \/ (Dir_of_Lines AS); definition let AS be AffinSpace; func ProjectiveLines AS -> non empty set equals :: AFPROJ:def 10 [:(AfLines AS),{1}:] \/ [:(Dir_of_Planes AS),{2}:]; coherence [:(AfLines AS),{1}:] \/ [:(Dir_of_Planes AS),{2}:] is non empty set ; end; :: deftheorem defines ProjectiveLines AFPROJ:def_10_:_ for AS being AffinSpace holds ProjectiveLines AS = [:(AfLines AS),{1}:] \/ [:(Dir_of_Planes AS),{2}:]; definition let AS be AffinSpace; func Proj_Inc AS -> Relation of (ProjectivePoints AS),(ProjectiveLines AS) means :Def11: :: AFPROJ:def 11 for x, y being set holds ( [x,y] in it iff ( ex K being Subset of AS st ( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st ( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ); existence ex b1 being Relation of (ProjectivePoints AS),(ProjectiveLines AS) st for x, y being set holds ( [x,y] in b1 iff ( ex K being Subset of AS st ( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st ( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) proofend; uniqueness for b1, b2 being Relation of (ProjectivePoints AS),(ProjectiveLines AS) st ( for x, y being set holds ( [x,y] in b1 iff ( ex K being Subset of AS st ( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st ( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) ) & ( for x, y being set holds ( [x,y] in b2 iff ( ex K being Subset of AS st ( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st ( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def11 defines Proj_Inc AFPROJ:def_11_:_ for AS being AffinSpace for b2 being Relation of (ProjectivePoints AS),(ProjectiveLines AS) holds ( b2 = Proj_Inc AS iff for x, y being set holds ( [x,y] in b2 iff ( ex K being Subset of AS st ( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st ( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) ); definition let AS be AffinSpace; func Inc_of_Dir AS -> Relation of (Dir_of_Lines AS),(Dir_of_Planes AS) means :Def12: :: AFPROJ:def 12 for x, y being set holds ( [x,y] in it iff ex A, X being Subset of AS st ( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ); existence ex b1 being Relation of (Dir_of_Lines AS),(Dir_of_Planes AS) st for x, y being set holds ( [x,y] in b1 iff ex A, X being Subset of AS st ( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) proofend; uniqueness for b1, b2 being Relation of (Dir_of_Lines AS),(Dir_of_Planes AS) st ( for x, y being set holds ( [x,y] in b1 iff ex A, X being Subset of AS st ( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) ) & ( for x, y being set holds ( [x,y] in b2 iff ex A, X being Subset of AS st ( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def12 defines Inc_of_Dir AFPROJ:def_12_:_ for AS being AffinSpace for b2 being Relation of (Dir_of_Lines AS),(Dir_of_Planes AS) holds ( b2 = Inc_of_Dir AS iff for x, y being set holds ( [x,y] in b2 iff ex A, X being Subset of AS st ( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) ); definition let AS be AffinSpace; func IncProjSp_of AS -> strict IncProjStr equals :: AFPROJ:def 13 IncProjStr(# (ProjectivePoints AS),(ProjectiveLines AS),(Proj_Inc AS) #); correctness coherence IncProjStr(# (ProjectivePoints AS),(ProjectiveLines AS),(Proj_Inc AS) #) is strict IncProjStr ; ; end; :: deftheorem defines IncProjSp_of AFPROJ:def_13_:_ for AS being AffinSpace holds IncProjSp_of AS = IncProjStr(# (ProjectivePoints AS),(ProjectiveLines AS),(Proj_Inc AS) #); definition let AS be AffinSpace; func ProjHorizon AS -> strict IncProjStr equals :: AFPROJ:def 14 IncProjStr(# (Dir_of_Lines AS),(Dir_of_Planes AS),(Inc_of_Dir AS) #); correctness coherence IncProjStr(# (Dir_of_Lines AS),(Dir_of_Planes AS),(Inc_of_Dir AS) #) is strict IncProjStr ; ; end; :: deftheorem defines ProjHorizon AFPROJ:def_14_:_ for AS being AffinSpace holds ProjHorizon AS = IncProjStr(# (Dir_of_Lines AS),(Dir_of_Planes AS),(Inc_of_Dir AS) #); theorem Th20: :: AFPROJ:20 for AS being AffinSpace for x being set holds ( x is POINT of (IncProjSp_of AS) iff ( x is Element of AS or ex X being Subset of AS st ( x = LDir X & X is being_line ) ) ) proofend; theorem :: AFPROJ:21 for AS being AffinSpace for x being set holds ( x is Element of the Points of (ProjHorizon AS) iff ex X being Subset of AS st ( x = LDir X & X is being_line ) ) by Th14; theorem Th22: :: AFPROJ:22 for AS being AffinSpace for x being set st x is Element of the Points of (ProjHorizon AS) holds x is POINT of (IncProjSp_of AS) proofend; theorem Th23: :: AFPROJ:23 for AS being AffinSpace for x being set holds ( x is LINE of (IncProjSp_of AS) iff ex X being Subset of AS st ( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) ) proofend; theorem :: AFPROJ:24 for AS being AffinSpace for x being set holds ( x is Element of the Lines of (ProjHorizon AS) iff ex X being Subset of AS st ( x = PDir X & X is being_plane ) ) by Th15; theorem Th25: :: AFPROJ:25 for AS being AffinSpace for x being set st x is Element of the Lines of (ProjHorizon AS) holds [x,2] is LINE of (IncProjSp_of AS) proofend; theorem Th26: :: AFPROJ:26 for AS being AffinSpace for x being Element of AS for X being Subset of AS for a being POINT of (IncProjSp_of AS) for A being LINE of (IncProjSp_of AS) st x = a & [X,1] = A holds ( a on A iff ( X is being_line & x in X ) ) proofend; theorem Th27: :: AFPROJ:27 for AS being AffinSpace for x being Element of AS for X being Subset of AS for a being POINT of (IncProjSp_of AS) for A being LINE of (IncProjSp_of AS) st x = a & [(PDir X),2] = A holds not a on A proofend; theorem Th28: :: AFPROJ:28 for AS being AffinSpace for Y, X being Subset of AS for a being POINT of (IncProjSp_of AS) for A being LINE of (IncProjSp_of AS) st a = LDir Y & [X,1] = A & Y is being_line & X is being_line holds ( a on A iff Y '||' X ) proofend; theorem Th29: :: AFPROJ:29 for AS being AffinSpace for Y, X being Subset of AS for a being POINT of (IncProjSp_of AS) for A being LINE of (IncProjSp_of AS) st a = LDir Y & A = [(PDir X),2] & Y is being_line & X is being_plane holds ( a on A iff Y '||' X ) proofend; theorem Th30: :: AFPROJ:30 for AS being AffinSpace for X being Subset of AS for a being POINT of (IncProjSp_of AS) for A being LINE of (IncProjSp_of AS) st X is being_line & a = LDir X & A = [X,1] holds a on A proofend; theorem Th31: :: AFPROJ:31 for AS being AffinSpace for X, Y being Subset of AS for a being POINT of (IncProjSp_of AS) for A being LINE of (IncProjSp_of AS) st X is being_line & Y is being_plane & X c= Y & a = LDir X & A = [(PDir Y),2] holds a on A proofend; theorem Th32: :: AFPROJ:32 for AS being AffinSpace for Y, X, X9 being Subset of AS for a being POINT of (IncProjSp_of AS) for A being LINE of (IncProjSp_of AS) st Y is being_plane & X c= Y & X9 // X & a = LDir X9 & A = [(PDir Y),2] holds a on A proofend; theorem :: AFPROJ:33 for AS being AffinSpace for X being Subset of AS for a being POINT of (IncProjSp_of AS) for A being LINE of (IncProjSp_of AS) st A = [(PDir X),2] & X is being_plane & a on A holds not a is Element of AS by Th27; theorem Th34: :: AFPROJ:34 for AS being AffinSpace for X being Subset of AS for p being POINT of (IncProjSp_of AS) for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is being_line & p on A & p is not Element of AS holds p = LDir X proofend; theorem Th35: :: AFPROJ:35 for AS being AffinSpace for X being Subset of AS for p, a being POINT of (IncProjSp_of AS) for A being LINE of (IncProjSp_of AS) st A = [X,1] & X is being_line & p on A & a on A & a <> p & p is not Element of AS holds a is Element of AS proofend; theorem Th36: :: AFPROJ:36 for AS being AffinSpace for X, Y being Subset of AS for a being Element of the Points of (ProjHorizon AS) for A being Element of the Lines of (ProjHorizon AS) st a = LDir X & A = PDir Y & X is being_line & Y is being_plane holds ( a on A iff X '||' Y ) proofend; theorem Th37: :: AFPROJ:37 for AS being AffinSpace for a being Element of the Points of (ProjHorizon AS) for a9 being Element of the Points of (IncProjSp_of AS) for A being Element of the Lines of (ProjHorizon AS) for A9 being LINE of (IncProjSp_of AS) st a9 = a & A9 = [A,2] holds ( a on A iff a9 on A9 ) proofend; theorem Th38: :: AFPROJ:38 for AS being AffinSpace for a, b being Element of the Points of (ProjHorizon AS) for A, K being Element of the Lines of (ProjHorizon AS) st a on A & a on K & b on A & b on K & not a = b holds A = K proofend; theorem Th39: :: AFPROJ:39 for AS being AffinSpace for A being Element of the Lines of (ProjHorizon AS) ex a, b, c being Element of the Points of (ProjHorizon AS) st ( a on A & b on A & c on A & a <> b & b <> c & c <> a ) proofend; theorem Th40: :: AFPROJ:40 for AS being AffinSpace for a, b being Element of the Points of (ProjHorizon AS) ex A being Element of the Lines of (ProjHorizon AS) st ( a on A & b on A ) proofend; Lm1: for AS being AffinSpace st AS is not AffinPlane holds ex a being Element of the Points of (ProjHorizon AS) ex A being Element of the Lines of (ProjHorizon AS) st not a on A proofend; Lm2: for AS being AffinSpace for a, b being POINT of (IncProjSp_of AS) for A, K being LINE of (IncProjSp_of AS) st a on A & a on K & b on A & b on K & not a = b holds A = K proofend; Lm3: for AS being AffinSpace for A being LINE of (IncProjSp_of AS) ex a, b, c being POINT of (IncProjSp_of AS) st ( a on A & b on A & c on A & a <> b & b <> c & c <> a ) proofend; Lm4: for AS being AffinSpace for a, b being POINT of (IncProjSp_of AS) ex A being LINE of (IncProjSp_of AS) st ( a on A & b on A ) proofend; Lm5: for AS being AffinSpace for A, K being LINE of (IncProjSp_of AS) st AS is AffinPlane holds ex a being POINT of (IncProjSp_of AS) st ( a on A & a on K ) proofend; Lm6: for AS being AffinSpace holds not for a being POINT of (IncProjSp_of AS) for A being LINE of (IncProjSp_of AS) holds a on A proofend; theorem Th41: :: AFPROJ:41 for AS being AffinSpace for x, y being Element of the Points of (ProjHorizon AS) for X being Element of the Lines of (IncProjSp_of AS) st x <> y & [x,X] in the Inc of (IncProjSp_of AS) & [y,X] in the Inc of (IncProjSp_of AS) holds ex Y being Element of the Lines of (ProjHorizon AS) st X = [Y,2] proofend; theorem Th42: :: AFPROJ:42 for AS being AffinSpace for x being POINT of (IncProjSp_of AS) for X being Element of the Lines of (ProjHorizon AS) st [x,[X,2]] in the Inc of (IncProjSp_of AS) holds x is Element of the Points of (ProjHorizon AS) proofend; Lm7: for AS being AffinSpace for X, X9, Y, Y9 being Subset of AS for b, c being POINT of (IncProjSp_of AS) for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [Y9,1] & Y9 is being_line holds Y9 c= Y proofend; Lm8: for AS being AffinSpace for X, X9, Y, Y9 being Subset of AS for b, c being POINT of (IncProjSp_of AS) for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [(PDir Y9),2] & Y9 is being_plane holds ( Y9 '||' Y & Y '||' Y9 ) proofend; theorem Th43: :: AFPROJ:43 for AS being AffinSpace for Y, X, X9 being Subset of AS for P, Q being LINE of (IncProjSp_of AS) st Y is being_plane & X is being_line & X9 is being_line & X c= Y & X9 c= Y & P = [X,1] & Q = [X9,1] holds ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) proofend; Lm9: for AS being AffinSpace for a, b, c, d, p being POINT of (IncProjSp_of AS) for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is Element of AS holds ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) proofend; Lm10: for AS being AffinSpace for a, b, c, d, p being POINT of (IncProjSp_of AS) for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is not Element of AS & a is Element of AS holds ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) proofend; Lm11: for AS being AffinSpace for a, b, c, d, p being POINT of (IncProjSp_of AS) for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is not Element of AS & ( a is Element of AS or b is Element of AS or c is Element of AS or d is Element of AS ) holds ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) proofend; Lm12: for AS being AffinSpace for a, b, c, d, p being POINT of (IncProjSp_of AS) for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) proofend; theorem Th44: :: AFPROJ:44 for AS being AffinSpace for a, b, c, d, p being Element of the Points of (ProjHorizon AS) for M, N, P, Q being Element of the Lines of (ProjHorizon AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds ex q being Element of the Points of (ProjHorizon AS) st ( q on P & q on Q ) proofend; registration let AS be AffinSpace; cluster IncProjSp_of AS -> strict linear partial up-2-dimensional up-3-rank Vebleian ; correctness coherence ( IncProjSp_of AS is partial & IncProjSp_of AS is linear & IncProjSp_of AS is up-2-dimensional & IncProjSp_of AS is up-3-rank & IncProjSp_of AS is Vebleian ); proofend; end; registration cluster strict linear partial up-2-dimensional up-3-rank Vebleian 2-dimensional for IncProjStr ; existence ex b1 being IncProjSp st ( b1 is strict & b1 is 2-dimensional ) proofend; end; registration let AS be AffinPlane; cluster IncProjSp_of AS -> strict 2-dimensional ; correctness coherence IncProjSp_of AS is 2-dimensional ; proofend; end; theorem :: AFPROJ:45 for AS being AffinSpace st IncProjSp_of AS is 2-dimensional holds AS is AffinPlane proofend; theorem :: AFPROJ:46 for AS being AffinSpace st AS is not AffinPlane holds ProjHorizon AS is IncProjSp proofend; theorem :: AFPROJ:47 for AS being AffinSpace st ProjHorizon AS is IncProjSp holds not AS is AffinPlane proofend; theorem Th48: :: AFPROJ:48 for AS being AffinSpace for M, N being Subset of AS for o, a, b, c, a9, b9, c9 being Element of AS st M is being_line & N is being_line & M <> N & o in M & o in N & o <> b & o <> b9 & o <> c9 & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & ( a = b or b = c or a = c ) holds a,c9 // c,a9 proofend; theorem :: AFPROJ:49 for AS being AffinSpace st IncProjSp_of AS is Pappian holds AS is Pappian proofend; theorem Th50: :: AFPROJ:50 for AS being AffinSpace for A, P, C being Subset of AS for o, a, b, c, a9, b9, c9 being Element of AS st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & ( o = a9 or a = a9 ) holds b,c // b9,c9 proofend; theorem :: AFPROJ:51 for AS being AffinSpace st IncProjSp_of AS is Desarguesian holds AS is Desarguesian proofend; theorem :: AFPROJ:52 for AS being AffinSpace st IncProjSp_of AS is Fanoian holds AS is Fanoian proofend;