:: AFPROJ semantic presentation begin 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 proof let AS be AffinSpace; ::_thesis: for X being Subset of AS st AS is AffinPlane & X = the carrier of AS holds X is being_plane let X be Subset of AS; ::_thesis: ( AS is AffinPlane & X = the carrier of AS implies X is being_plane ) assume that A1: AS is AffinPlane and A2: X = the carrier of AS ; ::_thesis: X is being_plane consider a, b, c being Element of AS such that A3: not LIN a,b,c by AFF_1:12; set P = Line (a,b); set K = Line (a,c); A4: b in Line (a,b) by AFF_1:15; A5: c in Line (a,c) by AFF_1:15; a <> b by A3, AFF_1:7; then A6: Line (a,b) is being_line by AFF_1:def_3; set Y = Plane ((Line (a,c)),(Line (a,b))); A7: a in Line (a,b) by AFF_1:15; a <> c by A3, AFF_1:7; then A8: Line (a,c) is being_line by AFF_1:def_3; A9: a in Line (a,c) by AFF_1:15; A10: not Line (a,c) // Line (a,b) proof assume Line (a,c) // Line (a,b) ; ::_thesis: contradiction then c in Line (a,b) by A7, A9, A5, AFF_1:45; hence contradiction by A3, A7, A4, A6, AFF_1:21; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_X_holds_ x_in_Plane_((Line_(a,c)),(Line_(a,b))) let x be set ; ::_thesis: ( x in X implies x in Plane ((Line (a,c)),(Line (a,b))) ) assume x in X ; ::_thesis: x in Plane ((Line (a,c)),(Line (a,b))) then reconsider a = x as Element of AS ; set K9 = a * (Line (a,c)); A11: a * (Line (a,c)) is being_line by A8, AFF_4:27; A12: Line (a,c) // a * (Line (a,c)) by A8, AFF_4:def_3; then not a * (Line (a,c)) // Line (a,b) by A10, AFF_1:44; then consider b being Element of AS such that A13: b in a * (Line (a,c)) and A14: b in Line (a,b) by A1, A6, A11, AFF_1:58; a in a * (Line (a,c)) by A8, AFF_4:def_3; then a,b // Line (a,c) by A12, A13, AFF_1:40; then a in { zz where zz is Element of AS : ex b being Element of AS st ( zz,b // Line (a,c) & b in Line (a,b) ) } by A14; hence x in Plane ((Line (a,c)),(Line (a,b))) by AFF_4:def_1; ::_thesis: verum end; then A15: X c= Plane ((Line (a,c)),(Line (a,b))) by TARSKI:def_3; Plane ((Line (a,c)),(Line (a,b))) is being_plane by A6, A8, A10, AFF_4:def_2; hence X is being_plane by A2, A15, XBOOLE_0:def_10; ::_thesis: verum end; 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 proof let AS be AffinSpace; ::_thesis: for X being Subset of AS st AS is AffinPlane & X is being_plane holds X = the carrier of AS let X be Subset of AS; ::_thesis: ( AS is AffinPlane & X is being_plane implies X = the carrier of AS ) assume that A1: AS is AffinPlane and A2: X is being_plane ; ::_thesis: X = the carrier of AS the carrier of AS c= the carrier of AS ; then reconsider Z = the carrier of AS as Subset of AS ; Z is being_plane by A1, Th1; hence X = the carrier of AS by A2, AFF_4:33; ::_thesis: verum end; 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 proof let AS be AffinSpace; ::_thesis: for X, Y being Subset of AS st AS is AffinPlane & X is being_plane & Y is being_plane holds X = Y let X, Y be Subset of AS; ::_thesis: ( AS is AffinPlane & X is being_plane & Y is being_plane implies X = Y ) assume that A1: AS is AffinPlane and A2: X is being_plane and A3: Y is being_plane ; ::_thesis: X = Y X = the carrier of AS by A1, A2, Th2; hence X = Y by A1, A3, Th2; ::_thesis: verum end; 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 proof let AS be AffinSpace; ::_thesis: for X being Subset of AS st X = the carrier of AS & X is being_plane holds AS is AffinPlane let X be Subset of AS; ::_thesis: ( X = the carrier of AS & X is being_plane implies AS is AffinPlane ) assume that A1: X = the carrier of AS and A2: X is being_plane ; ::_thesis: AS is AffinPlane assume AS is not AffinPlane ; ::_thesis: contradiction then not for zz being Element of AS holds zz in X by A2, AFF_4:48; hence contradiction by A1; ::_thesis: verum end; 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 proof let AS be AffinSpace; ::_thesis: 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 let A, K, X, Y be Subset of AS; ::_thesis: ( 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 implies X '||' Y ) assume that A1: not A // K and A2: A '||' X and A3: A '||' Y and A4: K '||' X and A5: K '||' Y and A6: A is being_line and A7: K is being_line and A8: X is being_plane and A9: Y is being_plane ; ::_thesis: X '||' Y set y = the Element of Y; set x = the Element of X; A10: Y <> {} by A9, AFF_4:59; A11: X <> {} by A8, AFF_4:59; then reconsider a = the Element of X, b = the Element of Y as Element of AS by A10, TARSKI:def_3; A12: K // a * K by A7, AFF_4:def_3; A13: A // a * A by A6, AFF_4:def_3; A14: not a * A // a * K proof assume a * A // a * K ; ::_thesis: contradiction then a * A // K by A12, AFF_1:44; hence contradiction by A1, A13, AFF_1:44; ::_thesis: verum end; a * K c= a + X by A4, A7, A8, AFF_4:68; then A15: a * K c= X by A8, A11, AFF_4:66; K // b * K by A7, AFF_4:def_3; then A16: a * K // b * K by A12, AFF_1:44; b * A c= b + Y by A3, A6, A9, AFF_4:68; then A17: b * A c= Y by A9, A10, AFF_4:66; A // b * A by A6, AFF_4:def_3; then A18: a * A // b * A by A13, AFF_1:44; b * K c= b + Y by A5, A7, A9, AFF_4:68; then A19: b * K c= Y by A9, A10, AFF_4:66; a * A c= a + X by A2, A6, A8, AFF_4:68; then a * A c= X by A8, A11, AFF_4:66; hence X '||' Y by A8, A9, A15, A17, A19, A14, A18, A16, AFF_4:55; ::_thesis: verum end; 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; 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 proof set X = { A where A is Subset of AS : A is being_line } ; { A where A is Subset of AS : A is being_line } c= bool the carrier of AS proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { A where A is Subset of AS : A is being_line } or x in bool the carrier of AS ) assume x in { A where A is Subset of AS : A is being_line } ; ::_thesis: x in bool the carrier of AS then ex A being Subset of AS st ( x = A & A is being_line ) ; hence x in bool the carrier of AS ; ::_thesis: verum end; hence { A where A is Subset of AS : A is being_line } is Subset-Family of AS ; ::_thesis: verum end; 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 proof set X = { A where A is Subset of AS : A is being_plane } ; { A where A is Subset of AS : A is being_plane } c= bool the carrier of AS proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { A where A is Subset of AS : A is being_plane } or x in bool the carrier of AS ) assume x in { A where A is Subset of AS : A is being_plane } ; ::_thesis: x in bool the carrier of AS then ex A being Subset of AS st ( x = A & A is being_plane ) ; hence x in bool the carrier of AS ; ::_thesis: verum end; hence { A where A is Subset of AS : A is being_plane } is Subset-Family of AS ; ::_thesis: verum end; 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) proof set AFL = AfLines AS; set AFL2 = [:(AfLines AS),(AfLines AS):]; set R1 = { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } ; now__::_thesis:_for_x_being_set_st_x_in__{__[X,Y]_where_X,_Y_is_Subset_of_AS_:_(_X_is_being_line_&_Y_is_being_line_&_X_'||'_Y_)__}__holds_ x_in_[:(AfLines_AS),(AfLines_AS):] let x be set ; ::_thesis: ( x in { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } implies x in [:(AfLines AS),(AfLines AS):] ) assume x in { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } ; ::_thesis: x in [:(AfLines AS),(AfLines AS):] then consider X, Y being Subset of AS such that A1: x = [X,Y] and A2: X is being_line and A3: Y is being_line and X '||' Y ; A4: Y in AfLines AS by A3; X in AfLines AS by A2; hence x in [:(AfLines AS),(AfLines AS):] by A1, A4, ZFMISC_1:def_2; ::_thesis: verum end; then reconsider R2 = { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } as Relation of (AfLines AS),(AfLines AS) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_AfLines_AS_holds_ [x,x]_in_R2 let x be set ; ::_thesis: ( x in AfLines AS implies [x,x] in R2 ) assume x in AfLines AS ; ::_thesis: [x,x] in R2 then consider X being Subset of AS such that A5: x = X and A6: X is being_line ; X // X by A6, AFF_1:41; then X '||' X by A6, AFF_4:40; hence [x,x] in R2 by A5, A6; ::_thesis: verum end; then A7: R2 is_reflexive_in AfLines AS by RELAT_2:def_1; then A8: field R2 = AfLines AS by ORDERS_1:13; A9: for X, Y being Subset of AS st X is being_line & Y is being_line holds ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } iff X '||' Y ) proof let X, Y be Subset of AS; ::_thesis: ( X is being_line & Y is being_line implies ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } iff X '||' Y ) ) assume that A10: X is being_line and A11: Y is being_line ; ::_thesis: ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } iff X '||' Y ) now__::_thesis:_(_[X,Y]_in__{__[X,Y]_where_X,_Y_is_Subset_of_AS_:_(_X_is_being_line_&_Y_is_being_line_&_X_'||'_Y_)__}__implies_X_'||'_Y_) assume [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } ; ::_thesis: X '||' Y then consider X9, Y9 being Subset of AS such that A12: [X,Y] = [X9,Y9] and X9 is being_line and Y9 is being_line and A13: X9 '||' Y9 ; X = X9 by A12, XTUPLE_0:1; hence X '||' Y by A12, A13, XTUPLE_0:1; ::_thesis: verum end; hence ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } iff X '||' Y ) by A10, A11; ::_thesis: verum end; now__::_thesis:_for_x,_y,_z_being_set_st_x_in_AfLines_AS_&_y_in_AfLines_AS_&_z_in_AfLines_AS_&_[x,y]_in_R2_&_[y,z]_in_R2_holds_ [x,z]_in_R2 let x, y, z be set ; ::_thesis: ( x in AfLines AS & y in AfLines AS & z in AfLines AS & [x,y] in R2 & [y,z] in R2 implies [x,z] in R2 ) assume that A14: x in AfLines AS and A15: y in AfLines AS and A16: z in AfLines AS and A17: [x,y] in R2 and A18: [y,z] in R2 ; ::_thesis: [x,z] in R2 consider Y being Subset of AS such that A19: y = Y and A20: Y is being_line by A15; consider Z being Subset of AS such that A21: z = Z and A22: Z is being_line by A16; Y '||' Z by A9, A18, A19, A20, A21, A22; then A23: Y // Z by A20, A22, AFF_4:40; consider X being Subset of AS such that A24: x = X and A25: X is being_line by A14; X '||' Y by A9, A17, A24, A25, A19, A20; then X // Y by A25, A20, AFF_4:40; then X // Z by A23, AFF_1:44; then X '||' Z by A25, A22, AFF_4:40; hence [x,z] in R2 by A24, A25, A21, A22; ::_thesis: verum end; then A26: R2 is_transitive_in AfLines AS by RELAT_2:def_8; now__::_thesis:_for_x,_y_being_set_st_x_in_AfLines_AS_&_y_in_AfLines_AS_&_[x,y]_in_R2_holds_ [y,x]_in_R2 let x, y be set ; ::_thesis: ( x in AfLines AS & y in AfLines AS & [x,y] in R2 implies [y,x] in R2 ) assume that A27: x in AfLines AS and A28: y in AfLines AS and A29: [x,y] in R2 ; ::_thesis: [y,x] in R2 consider X being Subset of AS such that A30: x = X and A31: X is being_line by A27; consider Y being Subset of AS such that A32: y = Y and A33: Y is being_line by A28; X '||' Y by A9, A29, A30, A31, A32, A33; then X // Y by A31, A33, AFF_4:40; then Y '||' X by A31, A33, AFF_4:40; hence [y,x] in R2 by A30, A31, A32, A33; ::_thesis: verum end; then A34: R2 is_symmetric_in AfLines AS by RELAT_2:def_3; dom R2 = AfLines AS by A7, ORDERS_1:13; hence { [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) by A8, A34, A26, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16; ::_thesis: verum end; 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) proof set AFP = AfPlanes AS; set AFP2 = [:(AfPlanes AS),(AfPlanes AS):]; set R1 = { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ; now__::_thesis:_for_x_being_set_st_x_in__{__[X,Y]_where_X,_Y_is_Subset_of_AS_:_(_X_is_being_plane_&_Y_is_being_plane_&_X_'||'_Y_)__}__holds_ x_in_[:(AfPlanes_AS),(AfPlanes_AS):] let x be set ; ::_thesis: ( x in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } implies x in [:(AfPlanes AS),(AfPlanes AS):] ) assume x in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ; ::_thesis: x in [:(AfPlanes AS),(AfPlanes AS):] then consider X, Y being Subset of AS such that A1: x = [X,Y] and A2: X is being_plane and A3: Y is being_plane and X '||' Y ; A4: Y in AfPlanes AS by A3; X in AfPlanes AS by A2; hence x in [:(AfPlanes AS),(AfPlanes AS):] by A1, A4, ZFMISC_1:def_2; ::_thesis: verum end; then reconsider R2 = { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } as Relation of (AfPlanes AS),(AfPlanes AS) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_AfPlanes_AS_holds_ [x,x]_in_R2 let x be set ; ::_thesis: ( x in AfPlanes AS implies [x,x] in R2 ) assume x in AfPlanes AS ; ::_thesis: [x,x] in R2 then consider X being Subset of AS such that A5: x = X and A6: X is being_plane ; X '||' X by A6, AFF_4:57; hence [x,x] in R2 by A5, A6; ::_thesis: verum end; then A7: R2 is_reflexive_in AfPlanes AS by RELAT_2:def_1; then A8: field R2 = AfPlanes AS by ORDERS_1:13; A9: for X, Y being Subset of AS st X is being_plane & Y is being_plane holds ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } iff X '||' Y ) proof let X, Y be Subset of AS; ::_thesis: ( X is being_plane & Y is being_plane implies ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } iff X '||' Y ) ) assume that A10: X is being_plane and A11: Y is being_plane ; ::_thesis: ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } iff X '||' Y ) now__::_thesis:_(_[X,Y]_in__{__[X,Y]_where_X,_Y_is_Subset_of_AS_:_(_X_is_being_plane_&_Y_is_being_plane_&_X_'||'_Y_)__}__implies_X_'||'_Y_) assume [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ; ::_thesis: X '||' Y then consider X9, Y9 being Subset of AS such that A12: [X,Y] = [X9,Y9] and X9 is being_plane and Y9 is being_plane and A13: X9 '||' Y9 ; X = X9 by A12, XTUPLE_0:1; hence X '||' Y by A12, A13, XTUPLE_0:1; ::_thesis: verum end; hence ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } iff X '||' Y ) by A10, A11; ::_thesis: verum end; now__::_thesis:_for_x,_y,_z_being_set_st_x_in_AfPlanes_AS_&_y_in_AfPlanes_AS_&_z_in_AfPlanes_AS_&_[x,y]_in_R2_&_[y,z]_in_R2_holds_ [x,z]_in_R2 let x, y, z be set ; ::_thesis: ( x in AfPlanes AS & y in AfPlanes AS & z in AfPlanes AS & [x,y] in R2 & [y,z] in R2 implies [x,z] in R2 ) assume that A14: x in AfPlanes AS and A15: y in AfPlanes AS and A16: z in AfPlanes AS and A17: [x,y] in R2 and A18: [y,z] in R2 ; ::_thesis: [x,z] in R2 consider X being Subset of AS such that A19: x = X and A20: X is being_plane by A14; consider Y being Subset of AS such that A21: y = Y and A22: Y is being_plane by A15; consider Z being Subset of AS such that A23: z = Z and A24: Z is being_plane by A16; A25: Y '||' Z by A9, A18, A21, A22, A23, A24; X '||' Y by A9, A17, A19, A20, A21, A22; then X '||' Z by A20, A22, A24, A25, AFF_4:61; hence [x,z] in R2 by A19, A20, A23, A24; ::_thesis: verum end; then A26: R2 is_transitive_in AfPlanes AS by RELAT_2:def_8; now__::_thesis:_for_x,_y_being_set_st_x_in_AfPlanes_AS_&_y_in_AfPlanes_AS_&_[x,y]_in_R2_holds_ [y,x]_in_R2 let x, y be set ; ::_thesis: ( x in AfPlanes AS & y in AfPlanes AS & [x,y] in R2 implies [y,x] in R2 ) assume that A27: x in AfPlanes AS and A28: y in AfPlanes AS and A29: [x,y] in R2 ; ::_thesis: [y,x] in R2 consider X being Subset of AS such that A30: x = X and A31: X is being_plane by A27; consider Y being Subset of AS such that A32: y = Y and A33: Y is being_plane by A28; X '||' Y by A9, A29, A30, A31, A32, A33; then Y '||' X by A31, A33, AFF_4:58; hence [y,x] in R2 by A30, A31, A32, A33; ::_thesis: verum end; then A34: R2 is_symmetric_in AfPlanes AS by RELAT_2:def_3; dom R2 = AfPlanes AS by A7, ORDERS_1:13; hence { [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) by A8, A34, A26, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16; ::_thesis: verum end; 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 ) ) proof let AS be AffinSpace; ::_thesis: 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 ) ) let X be Subset of AS; ::_thesis: ( X is being_line implies 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 ) ) ) assume A1: X is being_line ; ::_thesis: 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 ) ) let x be set ; ::_thesis: ( x in LDir X iff ex Y being Subset of AS st ( x = Y & Y is being_line & X '||' Y ) ) A2: now__::_thesis:_(_x_in_LDir_X_implies_ex_Y_being_Subset_of_AS_st_ (_x_=_Y_&_Y_is_being_line_&_X_'||'_Y_)_) assume x in LDir X ; ::_thesis: ex Y being Subset of AS st ( x = Y & Y is being_line & X '||' Y ) then [x,X] in LinesParallelity AS by EQREL_1:19; then consider K, M being Subset of AS such that A3: [x,X] = [K,M] and A4: K is being_line and A5: M is being_line and A6: K '||' M ; take Y = K; ::_thesis: ( x = Y & Y is being_line & X '||' Y ) A7: X = M by A3, XTUPLE_0:1; K // M by A4, A5, A6, AFF_4:40; hence ( x = Y & Y is being_line & X '||' Y ) by A3, A4, A5, A7, AFF_4:40, XTUPLE_0:1; ::_thesis: verum end; now__::_thesis:_(_ex_Y_being_Subset_of_AS_st_ (_x_=_Y_&_Y_is_being_line_&_X_'||'_Y_)_implies_x_in_LDir_X_) given Y being Subset of AS such that A8: x = Y and A9: Y is being_line and A10: X '||' Y ; ::_thesis: x in LDir X X // Y by A1, A9, A10, AFF_4:40; then Y '||' X by A1, A9, AFF_4:40; then [Y,X] in { [K,M] where K, M is Subset of AS : ( K is being_line & M is being_line & K '||' M ) } by A1, A9; hence x in LDir X by A8, EQREL_1:19; ::_thesis: verum end; hence ( x in LDir X iff ex Y being Subset of AS st ( x = Y & Y is being_line & X '||' Y ) ) by A2; ::_thesis: verum end; 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 ) ) proof let AS be AffinSpace; ::_thesis: 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 ) ) let X be Subset of AS; ::_thesis: ( X is being_plane implies 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 ) ) ) assume A1: X is being_plane ; ::_thesis: 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 ) ) let x be set ; ::_thesis: ( x in PDir X iff ex Y being Subset of AS st ( x = Y & Y is being_plane & X '||' Y ) ) A2: now__::_thesis:_(_x_in_PDir_X_implies_ex_Y_being_Subset_of_AS_st_ (_x_=_Y_&_Y_is_being_plane_&_X_'||'_Y_)_) assume x in PDir X ; ::_thesis: ex Y being Subset of AS st ( x = Y & Y is being_plane & X '||' Y ) then [x,X] in PlanesParallelity AS by EQREL_1:19; then consider K, M being Subset of AS such that A3: [x,X] = [K,M] and A4: K is being_plane and A5: M is being_plane and A6: K '||' M ; take Y = K; ::_thesis: ( x = Y & Y is being_plane & X '||' Y ) X = M by A3, XTUPLE_0:1; hence ( x = Y & Y is being_plane & X '||' Y ) by A3, A4, A5, A6, AFF_4:58, XTUPLE_0:1; ::_thesis: verum end; now__::_thesis:_(_ex_Y_being_Subset_of_AS_st_ (_x_=_Y_&_Y_is_being_plane_&_X_'||'_Y_)_implies_x_in_PDir_X_) given Y being Subset of AS such that A7: x = Y and A8: Y is being_plane and A9: X '||' Y ; ::_thesis: x in PDir X Y '||' X by A1, A8, A9, AFF_4:58; then [Y,X] in { [K,M] where K, M is Subset of AS : ( K is being_plane & M is being_plane & K '||' M ) } by A1, A8; hence x in PDir X by A7, EQREL_1:19; ::_thesis: verum end; hence ( x in PDir X iff ex Y being Subset of AS st ( x = Y & Y is being_plane & X '||' Y ) ) by A2; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: for X, Y being Subset of AS st X is being_line & Y is being_line holds ( LDir X = LDir Y iff X // Y ) let X, Y be Subset of AS; ::_thesis: ( X is being_line & Y is being_line implies ( LDir X = LDir Y iff X // Y ) ) assume that A1: X is being_line and A2: Y is being_line ; ::_thesis: ( LDir X = LDir Y iff X // Y ) A3: LDir Y = Class ((LinesParallelity AS),Y) ; A4: Y in AfLines AS by A2; A5: now__::_thesis:_(_LDir_X_=_LDir_Y_implies_X_//_Y_) assume LDir X = LDir Y ; ::_thesis: X // Y then X in Class ((LinesParallelity AS),Y) by A4, EQREL_1:23; then ex Y9 being Subset of AS st ( X = Y9 & Y9 is being_line & Y '||' Y9 ) by A2, A3, Th9; hence X // Y by A2, AFF_4:40; ::_thesis: verum end; A6: LDir X = Class ((LinesParallelity AS),X) ; A7: X in AfLines AS by A1; now__::_thesis:_(_X_//_Y_implies_LDir_X_=_LDir_Y_) assume X // Y ; ::_thesis: LDir X = LDir Y then X '||' Y by A1, A2, AFF_4:40; then Y in Class ((LinesParallelity AS),X) by A1, A2, A6, Th9; hence LDir X = LDir Y by A7, EQREL_1:23; ::_thesis: verum end; hence ( LDir X = LDir Y iff X // Y ) by A5; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: for X, Y being Subset of AS st X is being_line & Y is being_line holds ( LDir X = LDir Y iff X '||' Y ) let X, Y be Subset of AS; ::_thesis: ( X is being_line & Y is being_line implies ( LDir X = LDir Y iff X '||' Y ) ) assume that A1: X is being_line and A2: Y is being_line ; ::_thesis: ( LDir X = LDir Y iff X '||' Y ) ( LDir X = LDir Y iff X // Y ) by A1, A2, Th11; hence ( LDir X = LDir Y iff X '||' Y ) by A1, A2, AFF_4:40; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: for X, Y being Subset of AS st X is being_plane & Y is being_plane holds ( PDir X = PDir Y iff X '||' Y ) let X, Y be Subset of AS; ::_thesis: ( X is being_plane & Y is being_plane implies ( PDir X = PDir Y iff X '||' Y ) ) assume that A1: X is being_plane and A2: Y is being_plane ; ::_thesis: ( PDir X = PDir Y iff X '||' Y ) A3: PDir Y = Class ((PlanesParallelity AS),Y) ; A4: Y in AfPlanes AS by A2; A5: now__::_thesis:_(_PDir_X_=_PDir_Y_implies_X_'||'_Y_) assume PDir X = PDir Y ; ::_thesis: X '||' Y then X in Class ((PlanesParallelity AS),Y) by A4, EQREL_1:23; then ex Y9 being Subset of AS st ( X = Y9 & Y9 is being_plane & Y '||' Y9 ) by A2, A3, Th10; hence X '||' Y by A2, AFF_4:58; ::_thesis: verum end; A6: PDir X = Class ((PlanesParallelity AS),X) ; A7: X in AfPlanes AS by A1; now__::_thesis:_(_X_'||'_Y_implies_PDir_X_=_PDir_Y_) assume X '||' Y ; ::_thesis: PDir X = PDir Y then Y in Class ((PlanesParallelity AS),X) by A1, A2, A6, Th10; hence PDir X = PDir Y by A7, EQREL_1:23; ::_thesis: verum end; hence ( PDir X = PDir Y iff X '||' Y ) by A5; ::_thesis: verum end; 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 proof consider a, b being Element of AS such that A1: a <> b by DIRAF:40; set A = Line (a,b); Line (a,b) is being_line by A1, AFF_1:def_3; then Line (a,b) in AfLines AS ; then Class ((LinesParallelity AS),(Line (a,b))) in Class (LinesParallelity AS) by EQREL_1:def_3; hence Class (LinesParallelity AS) is non empty set ; ::_thesis: verum end; 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 proof set a = the Element of AS; consider A being Subset of AS such that the Element of AS in A and the Element of AS in A and the Element of AS in A and A1: A is being_plane by AFF_4:37; A in AfPlanes AS by A1; then Class ((PlanesParallelity AS),A) in Class (PlanesParallelity AS) by EQREL_1:def_3; hence Class (PlanesParallelity AS) is non empty set ; ::_thesis: verum end; 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 ) ) proof let AS be AffinSpace; ::_thesis: 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 ) ) let x be set ; ::_thesis: ( x in Dir_of_Lines AS iff ex X being Subset of AS st ( x = LDir X & X is being_line ) ) A1: now__::_thesis:_(_x_in_Dir_of_Lines_AS_implies_ex_X_being_Subset_of_AS_st_ (_x_=_LDir_X_&_X_is_being_line_)_) assume A2: x in Dir_of_Lines AS ; ::_thesis: ex X being Subset of AS st ( x = LDir X & X is being_line ) then reconsider x99 = x as Subset of (AfLines AS) ; consider x9 being set such that A3: x9 in AfLines AS and A4: x99 = Class ((LinesParallelity AS),x9) by A2, EQREL_1:def_3; consider X being Subset of AS such that A5: x9 = X and A6: X is being_line by A3; take X = X; ::_thesis: ( x = LDir X & X is being_line ) thus x = LDir X by A4, A5; ::_thesis: X is being_line thus X is being_line by A6; ::_thesis: verum end; now__::_thesis:_(_ex_X_being_Subset_of_AS_st_ (_x_=_LDir_X_&_X_is_being_line_)_implies_x_in_Dir_of_Lines_AS_) given X being Subset of AS such that A7: x = LDir X and A8: X is being_line ; ::_thesis: x in Dir_of_Lines AS X in AfLines AS by A8; hence x in Dir_of_Lines AS by A7, EQREL_1:def_3; ::_thesis: verum end; hence ( x in Dir_of_Lines AS iff ex X being Subset of AS st ( x = LDir X & X is being_line ) ) by A1; ::_thesis: verum end; 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 ) ) proof let AS be AffinSpace; ::_thesis: 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 ) ) let x be set ; ::_thesis: ( x in Dir_of_Planes AS iff ex X being Subset of AS st ( x = PDir X & X is being_plane ) ) A1: now__::_thesis:_(_x_in_Dir_of_Planes_AS_implies_ex_X_being_Subset_of_AS_st_ (_x_=_PDir_X_&_X_is_being_plane_)_) assume A2: x in Dir_of_Planes AS ; ::_thesis: ex X being Subset of AS st ( x = PDir X & X is being_plane ) then reconsider x99 = x as Subset of (AfPlanes AS) ; consider x9 being set such that A3: x9 in AfPlanes AS and A4: x99 = Class ((PlanesParallelity AS),x9) by A2, EQREL_1:def_3; consider X being Subset of AS such that A5: x9 = X and A6: X is being_plane by A3; take X = X; ::_thesis: ( x = PDir X & X is being_plane ) thus x = PDir X by A4, A5; ::_thesis: X is being_plane thus X is being_plane by A6; ::_thesis: verum end; now__::_thesis:_(_ex_X_being_Subset_of_AS_st_ (_x_=_PDir_X_&_X_is_being_plane_)_implies_x_in_Dir_of_Planes_AS_) given X being Subset of AS such that A7: x = PDir X and A8: X is being_plane ; ::_thesis: x in Dir_of_Planes AS X in AfPlanes AS by A8; hence x in Dir_of_Planes AS by A7, EQREL_1:def_3; ::_thesis: verum end; hence ( x in Dir_of_Planes AS iff ex X being Subset of AS st ( x = PDir X & X is being_plane ) ) by A1; ::_thesis: verum end; theorem Th16: :: AFPROJ:16 for AS being AffinSpace holds the carrier of AS misses Dir_of_Lines AS proof let AS be AffinSpace; ::_thesis: the carrier of AS misses Dir_of_Lines AS assume not the carrier of AS misses Dir_of_Lines AS ; ::_thesis: contradiction then consider x being set such that A1: x in the carrier of AS and A2: x in Dir_of_Lines AS by XBOOLE_0:3; reconsider a = x as Element of AS by A1; consider X being Subset of AS such that A3: x = LDir X and A4: X is being_line by A2, Th14; set A = a * X; A5: a * X is being_line by A4, AFF_4:27; X // a * X by A4, AFF_4:def_3; then X '||' a * X by A4, A5, AFF_4:40; then a * X in x by A3, A4, A5, Th9; hence contradiction by A4, AFF_4:def_3; ::_thesis: verum end; theorem :: AFPROJ:17 for AS being AffinSpace st AS is AffinPlane holds AfLines AS misses Dir_of_Planes AS proof let AS be AffinSpace; ::_thesis: ( AS is AffinPlane implies AfLines AS misses Dir_of_Planes AS ) the carrier of AS c= the carrier of AS ; then reconsider X9 = the carrier of AS as Subset of AS ; assume AS is AffinPlane ; ::_thesis: AfLines AS misses Dir_of_Planes AS then A1: X9 is being_plane by Th1; assume not AfLines AS misses Dir_of_Planes AS ; ::_thesis: contradiction then consider x being set such that A2: x in AfLines AS and A3: x in Dir_of_Planes AS by XBOOLE_0:3; consider Y being Subset of AS such that A4: x = Y and A5: Y is being_line by A2; consider X being Subset of AS such that A6: x = PDir X and A7: X is being_plane by A3, Th15; consider a, b being Element of AS such that A8: a in Y and b in Y and a <> b by A5, AFF_1:19; consider Y9 being Subset of AS such that A9: a = Y9 and A10: Y9 is being_plane and X '||' Y9 by A6, A7, A4, A8, Th10; A11: not Y9 in Y9 ; Y9 = X9 by A1, A10, AFF_4:33; hence contradiction by A9, A11; ::_thesis: verum end; 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 ) ) proof let AS be AffinSpace; ::_thesis: 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 ) ) let x be set ; ::_thesis: ( x in [:(AfLines AS),{1}:] iff ex X being Subset of AS st ( x = [X,1] & X is being_line ) ) A1: now__::_thesis:_(_x_in_[:(AfLines_AS),{1}:]_implies_ex_X_being_Subset_of_AS_st_ (_x_=_[X,1]_&_X_is_being_line_)_) assume x in [:(AfLines AS),{1}:] ; ::_thesis: ex X being Subset of AS st ( x = [X,1] & X is being_line ) then consider x1, x2 being set such that A2: x1 in AfLines AS and A3: x2 in {1} and A4: x = [x1,x2] by ZFMISC_1:def_2; consider X being Subset of AS such that A5: x1 = X and A6: X is being_line by A2; take X = X; ::_thesis: ( x = [X,1] & X is being_line ) thus x = [X,1] by A3, A4, A5, TARSKI:def_1; ::_thesis: X is being_line thus X is being_line by A6; ::_thesis: verum end; now__::_thesis:_(_ex_X_being_Subset_of_AS_st_ (_x_=_[X,1]_&_X_is_being_line_)_implies_x_in_[:(AfLines_AS),{1}:]_) given X being Subset of AS such that A7: x = [X,1] and A8: X is being_line ; ::_thesis: x in [:(AfLines AS),{1}:] X in AfLines AS by A8; hence x in [:(AfLines AS),{1}:] by A7, ZFMISC_1:106; ::_thesis: verum end; hence ( x in [:(AfLines AS),{1}:] iff ex X being Subset of AS st ( x = [X,1] & X is being_line ) ) by A1; ::_thesis: verum end; 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 ) ) proof let AS be AffinSpace; ::_thesis: 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 ) ) let x be set ; ::_thesis: ( x in [:(Dir_of_Planes AS),{2}:] iff ex X being Subset of AS st ( x = [(PDir X),2] & X is being_plane ) ) A1: now__::_thesis:_(_x_in_[:(Dir_of_Planes_AS),{2}:]_implies_ex_X_being_Subset_of_AS_st_ (_x_=_[(PDir_X),2]_&_X_is_being_plane_)_) assume x in [:(Dir_of_Planes AS),{2}:] ; ::_thesis: ex X being Subset of AS st ( x = [(PDir X),2] & X is being_plane ) then consider x1, x2 being set such that A2: x1 in Dir_of_Planes AS and A3: x2 in {2} and A4: x = [x1,x2] by ZFMISC_1:def_2; consider X being Subset of AS such that A5: x1 = PDir X and A6: X is being_plane by A2, Th15; take X = X; ::_thesis: ( x = [(PDir X),2] & X is being_plane ) thus x = [(PDir X),2] by A3, A4, A5, TARSKI:def_1; ::_thesis: X is being_plane thus X is being_plane by A6; ::_thesis: verum end; now__::_thesis:_(_ex_X_being_Subset_of_AS_st_ (_x_=_[(PDir_X),2]_&_X_is_being_plane_)_implies_x_in_[:(Dir_of_Planes_AS),{2}:]_) given X being Subset of AS such that A7: x = [(PDir X),2] and A8: X is being_plane ; ::_thesis: x in [:(Dir_of_Planes AS),{2}:] PDir X in Dir_of_Planes AS by A8, Th15; hence x in [:(Dir_of_Planes AS),{2}:] by A7, ZFMISC_1:106; ::_thesis: verum end; hence ( x in [:(Dir_of_Planes AS),{2}:] iff ex X being Subset of AS st ( x = [(PDir X),2] & X is being_plane ) ) by A1; ::_thesis: verum end; 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 ) ) ) proof defpred S1[ set , set ] means ( ex K being Subset of AS st ( K is being_line & $2 = [K,1] & ( ( $1 in the carrier of AS & $1 in K ) or $1 = LDir K ) ) or ex K, X being Subset of AS st ( K is being_line & X is being_plane & $1 = LDir K & $2 = [(PDir X),2] & K '||' X ) ); set VV1 = ProjectivePoints AS; set VV2 = ProjectiveLines AS; consider P being Relation of (ProjectivePoints AS),(ProjectiveLines AS) such that A1: for x, y being set holds ( [x,y] in P iff ( x in ProjectivePoints AS & y in ProjectiveLines AS & S1[x,y] ) ) from RELSET_1:sch_1(); take P ; ::_thesis: for x, y being set holds ( [x,y] in P 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 ) ) ) let x, y be set ; ::_thesis: ( [x,y] in P 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 ) ) ) thus ( not [x,y] in P or 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 ) ) by A1; ::_thesis: ( ( 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 ) ) implies [x,y] in P ) assume A2: ( 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 ) ) ; ::_thesis: [x,y] in P ( x in ProjectivePoints AS & y in ProjectiveLines AS ) proof A3: now__::_thesis:_(_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_)_)_implies_(_x_in_ProjectivePoints_AS_&_y_in_ProjectiveLines_AS_)_) given K being Subset of AS such that A4: K is being_line and A5: y = [K,1] and A6: ( ( x in the carrier of AS & x in K ) or x = LDir K ) ; ::_thesis: ( x in ProjectivePoints AS & y in ProjectiveLines AS ) A7: now__::_thesis:_(_x_=_LDir_K_implies_x_in_ProjectivePoints_AS_) assume x = LDir K ; ::_thesis: x in ProjectivePoints AS then x in Dir_of_Lines AS by A4, Th14; hence x in ProjectivePoints AS by XBOOLE_0:def_3; ::_thesis: verum end; y in [:(AfLines AS),{1}:] by A4, A5, Th18; hence ( x in ProjectivePoints AS & y in ProjectiveLines AS ) by A6, A7, XBOOLE_0:def_3; ::_thesis: verum end; now__::_thesis:_(_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_)_implies_(_x_in_ProjectivePoints_AS_&_y_in_ProjectiveLines_AS_)_) given K, X being Subset of AS such that A8: K is being_line and A9: X is being_plane and A10: x = LDir K and A11: y = [(PDir X),2] and K '||' X ; ::_thesis: ( x in ProjectivePoints AS & y in ProjectiveLines AS ) x in Dir_of_Lines AS by A8, A10, Th14; hence x in ProjectivePoints AS by XBOOLE_0:def_3; ::_thesis: y in ProjectiveLines AS y in [:(Dir_of_Planes AS),{2}:] by A9, A11, Th19; hence y in ProjectiveLines AS by XBOOLE_0:def_3; ::_thesis: verum end; hence ( x in ProjectivePoints AS & y in ProjectiveLines AS ) by A2, A3; ::_thesis: verum end; hence [x,y] in P by A1, A2; ::_thesis: verum end; 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 proof let P, Q be Relation of (ProjectivePoints AS),(ProjectiveLines AS); ::_thesis: ( ( for x, y being set holds ( [x,y] in P 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 Q 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 ) ) ) ) implies P = Q ) assume that A12: for x, y being set holds ( [x,y] in P 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 ) ) ) and A13: for x, y being set holds ( [x,y] in Q 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 ) ) ) ; ::_thesis: P = Q for x, y being set holds ( [x,y] in P iff [x,y] in Q ) proof let x, y be set ; ::_thesis: ( [x,y] in P iff [x,y] in Q ) ( [x,y] in P 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 ) ) ) by A12; hence ( [x,y] in P iff [x,y] in Q ) by A13; ::_thesis: verum end; hence P = Q by RELAT_1:def_2; ::_thesis: verum end; 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 ) ) proof defpred S1[ set , set ] means ex A, X being Subset of AS st ( $1 = LDir A & $2 = PDir X & A is being_line & X is being_plane & A '||' X ); set VV1 = Dir_of_Lines AS; set VV2 = Dir_of_Planes AS; consider P being Relation of (Dir_of_Lines AS),(Dir_of_Planes AS) such that A1: for x, y being set holds ( [x,y] in P iff ( x in Dir_of_Lines AS & y in Dir_of_Planes AS & S1[x,y] ) ) from RELSET_1:sch_1(); take P ; ::_thesis: for x, y being set holds ( [x,y] in P 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 ) ) let x, y be set ; ::_thesis: ( [x,y] in P 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 ) ) thus ( [x,y] in P implies ex A, X being Subset of AS st ( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) by A1; ::_thesis: ( ex A, X being Subset of AS st ( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) implies [x,y] in P ) assume A2: ex A, X being Subset of AS st ( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ; ::_thesis: [x,y] in P then A3: y in Dir_of_Planes AS by Th15; x in Dir_of_Lines AS by A2, Th14; hence [x,y] in P by A1, A2, A3; ::_thesis: verum end; 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 proof let P, Q be Relation of (Dir_of_Lines AS),(Dir_of_Planes AS); ::_thesis: ( ( for x, y being set holds ( [x,y] in P 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 Q 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 ) ) ) implies P = Q ) assume that A4: for x, y being set holds ( [x,y] in P 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 ) ) and A5: for x, y being set holds ( [x,y] in Q 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 ) ) ; ::_thesis: P = Q for x, y being set holds ( [x,y] in P iff [x,y] in Q ) proof let x, y be set ; ::_thesis: ( [x,y] in P iff [x,y] in Q ) ( [x,y] in P 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 ) ) by A4; hence ( [x,y] in P iff [x,y] in Q ) by A5; ::_thesis: verum end; hence P = Q by RELAT_1:def_2; ::_thesis: verum end; 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 ) ) ) proof let AS be AffinSpace; ::_thesis: 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 ) ) ) let x be set ; ::_thesis: ( 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 ) ) ) A1: now__::_thesis:_(_(_x_is_Element_of_AS_or_ex_X_being_Subset_of_AS_st_ (_x_=_LDir_X_&_X_is_being_line_)_)_implies_x_is_POINT_of_(IncProjSp_of_AS)_) A2: now__::_thesis:_(_ex_X_being_Subset_of_AS_st_ (_x_=_LDir_X_&_X_is_being_line_)_implies_x_is_POINT_of_(IncProjSp_of_AS)_) given X being Subset of AS such that A3: x = LDir X and A4: X is being_line ; ::_thesis: x is POINT of (IncProjSp_of AS) x in Dir_of_Lines AS by A3, A4, Th14; hence x is POINT of (IncProjSp_of AS) by XBOOLE_0:def_3; ::_thesis: verum end; assume ( x is Element of AS or ex X being Subset of AS st ( x = LDir X & X is being_line ) ) ; ::_thesis: x is POINT of (IncProjSp_of AS) hence x is POINT of (IncProjSp_of AS) by A2, XBOOLE_0:def_3; ::_thesis: verum end; now__::_thesis:_(_not_x_is_POINT_of_(IncProjSp_of_AS)_or_x_is_Element_of_AS_or_ex_X_being_Subset_of_AS_st_ (_x_=_LDir_X_&_X_is_being_line_)_) assume A5: x is POINT of (IncProjSp_of AS) ; ::_thesis: ( x is Element of AS or ex X being Subset of AS st ( x = LDir X & X is being_line ) ) ( x in Dir_of_Lines AS implies ex X being Subset of AS st ( x = LDir X & X is being_line ) ) by Th14; hence ( x is Element of AS or ex X being Subset of AS st ( x = LDir X & X is being_line ) ) by A5, XBOOLE_0:def_3; ::_thesis: verum end; hence ( 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 ) ) ) by A1; ::_thesis: verum end; 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) proof let AS be AffinSpace; ::_thesis: for x being set st x is Element of the Points of (ProjHorizon AS) holds x is POINT of (IncProjSp_of AS) let x be set ; ::_thesis: ( x is Element of the Points of (ProjHorizon AS) implies x is POINT of (IncProjSp_of AS) ) assume x is Element of the Points of (ProjHorizon AS) ; ::_thesis: x is POINT of (IncProjSp_of AS) then ex X being Subset of AS st ( x = LDir X & X is being_line ) by Th14; hence x is POINT of (IncProjSp_of AS) by Th20; ::_thesis: verum end; 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 ) ) ) proof let AS be AffinSpace; ::_thesis: 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 ) ) ) let x be set ; ::_thesis: ( 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 ) ) ) A1: now__::_thesis:_(_ex_X_being_Subset_of_AS_st_ (_(_x_=_[X,1]_&_X_is_being_line_)_or_(_x_=_[(PDir_X),2]_&_X_is_being_plane_)_)_implies_x_is_LINE_of_(IncProjSp_of_AS)_) given X being Subset of AS such that A2: ( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) ; ::_thesis: x is LINE of (IncProjSp_of AS) A3: now__::_thesis:_(_x_=_[(PDir_X),2]_&_X_is_being_plane_implies_x_is_LINE_of_(IncProjSp_of_AS)_) assume that A4: x = [(PDir X),2] and A5: X is being_plane ; ::_thesis: x is LINE of (IncProjSp_of AS) x in [:(Dir_of_Planes AS),{2}:] by A4, A5, Th19; hence x is LINE of (IncProjSp_of AS) by XBOOLE_0:def_3; ::_thesis: verum end; now__::_thesis:_(_x_=_[X,1]_&_X_is_being_line_implies_x_is_LINE_of_(IncProjSp_of_AS)_) assume that A6: x = [X,1] and A7: X is being_line ; ::_thesis: x is LINE of (IncProjSp_of AS) x in [:(AfLines AS),{1}:] by A6, A7, Th18; hence x is LINE of (IncProjSp_of AS) by XBOOLE_0:def_3; ::_thesis: verum end; hence x is LINE of (IncProjSp_of AS) by A2, A3; ::_thesis: verum end; now__::_thesis:_(_x_is_LINE_of_(IncProjSp_of_AS)_implies_ex_X_being_Subset_of_AS_st_ (_(_x_=_[X,1]_&_X_is_being_line_)_or_(_x_=_[(PDir_X),2]_&_X_is_being_plane_)_)_) A8: ( x in [:(Dir_of_Planes AS),{2}:] implies ex X being Subset of AS st ( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) ) by Th19; assume A9: x is LINE of (IncProjSp_of AS) ; ::_thesis: ex X being Subset of AS st ( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) ( x in [:(AfLines AS),{1}:] implies ex X being Subset of AS st ( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) ) by Th18; hence ex X being Subset of AS st ( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) by A9, A8, XBOOLE_0:def_3; ::_thesis: verum end; hence ( 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 ) ) ) by A1; ::_thesis: verum end; 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) proof let AS be AffinSpace; ::_thesis: for x being set st x is Element of the Lines of (ProjHorizon AS) holds [x,2] is LINE of (IncProjSp_of AS) let x be set ; ::_thesis: ( x is Element of the Lines of (ProjHorizon AS) implies [x,2] is LINE of (IncProjSp_of AS) ) assume x is Element of the Lines of (ProjHorizon AS) ; ::_thesis: [x,2] is LINE of (IncProjSp_of AS) then ex X being Subset of AS st ( x = PDir X & X is being_plane ) by Th15; hence [x,2] is LINE of (IncProjSp_of AS) by Th23; ::_thesis: verum end; 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 ) ) proof let AS be AffinSpace; ::_thesis: 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 ) ) let x be Element of AS; ::_thesis: 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 ) ) let X be Subset of AS; ::_thesis: 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 ) ) let a be POINT of (IncProjSp_of AS); ::_thesis: 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 ) ) let A be LINE of (IncProjSp_of AS); ::_thesis: ( x = a & [X,1] = A implies ( a on A iff ( X is being_line & x in X ) ) ) assume that A1: x = a and A2: [X,1] = A ; ::_thesis: ( a on A iff ( X is being_line & x in X ) ) A3: now__::_thesis:_(_a_on_A_implies_(_X_is_being_line_&_x_in_X_)_) A4: now__::_thesis:_(_ex_K_being_Subset_of_AS_st_ (_K_is_being_line_&_[X,1]_=_[K,1]_&_(_(_x_in_the_carrier_of_AS_&_x_in_K_)_or_x_=_LDir_K_)_)_implies_(_X_is_being_line_&_x_in_X_)_) given K being Subset of AS such that A5: K is being_line and A6: [X,1] = [K,1] and A7: ( ( x in the carrier of AS & x in K ) or x = LDir K ) ; ::_thesis: ( X is being_line & x in X ) A8: now__::_thesis:_not_x_=_LDir_K assume x = LDir K ; ::_thesis: contradiction then x in Dir_of_Lines AS by A5, Th14; then the carrier of AS /\ (Dir_of_Lines AS) <> {} by XBOOLE_0:def_4; then the carrier of AS meets Dir_of_Lines AS by XBOOLE_0:def_7; hence contradiction by Th16; ::_thesis: verum end; X = [K,1] `1 by A6, MCART_1:7 .= K ; hence ( X is being_line & x in X ) by A5, A7, A8; ::_thesis: verum end; assume a on A ; ::_thesis: ( X is being_line & x in X ) then A9: [a,A] in the Inc of (IncProjSp_of AS) by INCSP_1:def_1; for K, X9 being Subset of AS holds ( not K is being_line or not X9 is being_plane or not x = LDir K or not [X,1] = [(PDir X9),2] or not K '||' X9 ) by XTUPLE_0:1; hence ( X is being_line & x in X ) by A1, A2, A9, A4, Def11; ::_thesis: verum end; now__::_thesis:_(_X_is_being_line_&_x_in_X_implies_a_on_A_) assume that A10: X is being_line and A11: x in X ; ::_thesis: a on A [x,[X,1]] in Proj_Inc AS by A10, A11, Def11; hence a on A by A1, A2, INCSP_1:def_1; ::_thesis: verum end; hence ( a on A iff ( X is being_line & x in X ) ) by A3; ::_thesis: verum end; 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 proof let AS be AffinSpace; ::_thesis: 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 let x be Element of AS; ::_thesis: 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 let X be Subset of AS; ::_thesis: 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 let a be POINT of (IncProjSp_of AS); ::_thesis: for A being LINE of (IncProjSp_of AS) st x = a & [(PDir X),2] = A holds not a on A let A be LINE of (IncProjSp_of AS); ::_thesis: ( x = a & [(PDir X),2] = A implies not a on A ) assume that A1: x = a and A2: [(PDir X),2] = A ; ::_thesis: not a on A A3: now__::_thesis:_for_K_being_Subset_of_AS_holds_ (_not_K_is_being_line_or_not_[(PDir_X),2]_=_[K,1]_or_(_not_(_x_in_the_carrier_of_AS_&_x_in_K_)_&_not_x_=_LDir_K_)_) given K being Subset of AS such that K is being_line and A4: [(PDir X),2] = [K,1] and ( ( x in the carrier of AS & x in K ) or x = LDir K ) ; ::_thesis: contradiction 2 = [K,1] `2 by A4, MCART_1:7 .= 1 ; hence contradiction ; ::_thesis: verum end; A5: now__::_thesis:_for_K,_X9_being_Subset_of_AS_holds_ (_not_K_is_being_line_or_not_X9_is_being_plane_or_not_x_=_LDir_K_or_not_[(PDir_X),2]_=_[(PDir_X9),2]_or_not_K_'||'_X9_) given K, X9 being Subset of AS such that A6: K is being_line and X9 is being_plane and A7: x = LDir K and [(PDir X),2] = [(PDir X9),2] and K '||' X9 ; ::_thesis: contradiction x in Dir_of_Lines AS by A6, A7, Th14; then the carrier of AS /\ (Dir_of_Lines AS) <> {} by XBOOLE_0:def_4; then the carrier of AS meets Dir_of_Lines AS by XBOOLE_0:def_7; hence contradiction by Th16; ::_thesis: verum end; assume a on A ; ::_thesis: contradiction then [a,A] in the Inc of (IncProjSp_of AS) by INCSP_1:def_1; hence contradiction by A1, A2, A3, A5, Def11; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let Y, X be Subset of AS; ::_thesis: 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 ) let a be POINT of (IncProjSp_of AS); ::_thesis: 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 ) let A be LINE of (IncProjSp_of AS); ::_thesis: ( a = LDir Y & [X,1] = A & Y is being_line & X is being_line implies ( a on A iff Y '||' X ) ) assume that A1: a = LDir Y and A2: [X,1] = A and A3: Y is being_line and A4: X is being_line ; ::_thesis: ( a on A iff Y '||' X ) A5: now__::_thesis:_(_a_on_A_implies_Y_'||'_X_) A6: now__::_thesis:_(_ex_K_being_Subset_of_AS_st_ (_K_is_being_line_&_[X,1]_=_[K,1]_&_(_(_LDir_Y_in_the_carrier_of_AS_&_LDir_Y_in_K_)_or_LDir_Y_=_LDir_K_)_)_implies_Y_'||'_X_) given K being Subset of AS such that A7: K is being_line and A8: [X,1] = [K,1] and A9: ( ( LDir Y in the carrier of AS & LDir Y in K ) or LDir Y = LDir K ) ; ::_thesis: Y '||' X A10: K in AfLines AS by A7; A11: X = K by A8, XTUPLE_0:1; A12: now__::_thesis:_(_LDir_Y_=_LDir_K_implies_Y_'||'_X_) assume LDir Y = LDir K ; ::_thesis: Y '||' X then A13: Y in Class ((LinesParallelity AS),K) by A10, EQREL_1:23; LDir K = Class ((LinesParallelity AS),K) ; then consider K9 being Subset of AS such that A14: Y = K9 and A15: K9 is being_line and A16: K '||' K9 by A7, A13, Th9; K // K9 by A7, A15, A16, AFF_4:40; hence Y '||' X by A7, A11, A14, A15, AFF_4:40; ::_thesis: verum end; now__::_thesis:_(_LDir_Y_in_the_carrier_of_AS_implies_not_LDir_Y_in_K_) assume that A17: LDir Y in the carrier of AS and LDir Y in K ; ::_thesis: contradiction a in Dir_of_Lines AS by A1, A3, Th14; then the carrier of AS /\ (Dir_of_Lines AS) <> {} by A1, A17, XBOOLE_0:def_4; then the carrier of AS meets Dir_of_Lines AS by XBOOLE_0:def_7; hence contradiction by Th16; ::_thesis: verum end; hence Y '||' X by A9, A12; ::_thesis: verum end; assume a on A ; ::_thesis: Y '||' X then A18: [a,A] in the Inc of (IncProjSp_of AS) by INCSP_1:def_1; for K, X9 being Subset of AS holds ( not K is being_line or not X9 is being_plane or not LDir Y = LDir K or not [X,1] = [(PDir X9),2] or not K '||' X9 ) by XTUPLE_0:1; hence Y '||' X by A1, A2, A18, A6, Def11; ::_thesis: verum end; now__::_thesis:_(_Y_'||'_X_implies_a_on_A_) assume Y '||' X ; ::_thesis: a on A then A19: X in LDir Y by A3, A4, Th9; A20: LDir X = Class ((LinesParallelity AS),X) ; Y in AfLines AS by A3; then Class ((LinesParallelity AS),X) = Class ((LinesParallelity AS),Y) by A19, EQREL_1:23; then [a,A] in Proj_Inc AS by A1, A2, A4, A20, Def11; hence a on A by INCSP_1:def_1; ::_thesis: verum end; hence ( a on A iff Y '||' X ) by A5; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let Y, X be Subset of AS; ::_thesis: 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 ) let a be POINT of (IncProjSp_of AS); ::_thesis: 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 ) let A be LINE of (IncProjSp_of AS); ::_thesis: ( a = LDir Y & A = [(PDir X),2] & Y is being_line & X is being_plane implies ( a on A iff Y '||' X ) ) assume that A1: a = LDir Y and A2: A = [(PDir X),2] and A3: Y is being_line and A4: X is being_plane ; ::_thesis: ( a on A iff Y '||' X ) A5: now__::_thesis:_(_a_on_A_implies_Y_'||'_X_) A6: now__::_thesis:_(_ex_K,_X9_being_Subset_of_AS_st_ (_K_is_being_line_&_X9_is_being_plane_&_LDir_Y_=_LDir_K_&_[(PDir_X),2]_=_[(PDir_X9),2]_&_K_'||'_X9_)_implies_Y_'||'_X_) given K, X9 being Subset of AS such that A7: K is being_line and A8: X9 is being_plane and A9: LDir Y = LDir K and A10: [(PDir X),2] = [(PDir X9),2] and A11: K '||' X9 ; ::_thesis: Y '||' X A12: X9 in AfPlanes AS by A8; A13: Class ((PlanesParallelity AS),X9) = PDir X9 ; PDir X = PDir X9 by A10, XTUPLE_0:1; then X in Class ((PlanesParallelity AS),X9) by A12, EQREL_1:23; then A14: ex X99 being Subset of AS st ( X = X99 & X99 is being_plane & X9 '||' X99 ) by A8, A13, Th10; K in AfLines AS by A7; then A15: Y in Class ((LinesParallelity AS),K) by A9, EQREL_1:23; Class ((LinesParallelity AS),K) = LDir K ; then consider K9 being Subset of AS such that A16: Y = K9 and A17: K9 is being_line and A18: K '||' K9 by A7, A15, Th9; K // K9 by A7, A17, A18, AFF_4:40; then K9 '||' X9 by A11, AFF_4:56; hence Y '||' X by A8, A16, A14, AFF_4:59, AFF_4:60; ::_thesis: verum end; assume a on A ; ::_thesis: Y '||' X then A19: [a,A] in the Inc of (IncProjSp_of AS) by INCSP_1:def_1; for K being Subset of AS holds ( not K is being_line or not [(PDir X),2] = [K,1] or ( not ( LDir Y in the carrier of AS & LDir Y in K ) & not LDir Y = LDir K ) ) by XTUPLE_0:1; hence Y '||' X by A1, A2, A19, A6, Def11; ::_thesis: verum end; now__::_thesis:_(_Y_'||'_X_implies_a_on_A_) assume Y '||' X ; ::_thesis: a on A then [(LDir Y),[(PDir X),2]] in Proj_Inc AS by A3, A4, Def11; hence a on A by A1, A2, INCSP_1:def_1; ::_thesis: verum end; hence ( a on A iff Y '||' X ) by A5; ::_thesis: verum end; 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 proof let AS be AffinSpace; ::_thesis: 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 let X be Subset of AS; ::_thesis: 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 let a be POINT of (IncProjSp_of AS); ::_thesis: for A being LINE of (IncProjSp_of AS) st X is being_line & a = LDir X & A = [X,1] holds a on A let A be LINE of (IncProjSp_of AS); ::_thesis: ( X is being_line & a = LDir X & A = [X,1] implies a on A ) assume that A1: X is being_line and A2: a = LDir X and A3: A = [X,1] ; ::_thesis: a on A X // X by A1, AFF_1:41; then X '||' X by A1, AFF_4:40; hence a on A by A1, A2, A3, Th28; ::_thesis: verum end; 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 proof let AS be AffinSpace; ::_thesis: 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 let X, Y be Subset of AS; ::_thesis: 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 let a be POINT of (IncProjSp_of AS); ::_thesis: 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 let A be LINE of (IncProjSp_of AS); ::_thesis: ( X is being_line & Y is being_plane & X c= Y & a = LDir X & A = [(PDir Y),2] implies a on A ) assume that A1: X is being_line and A2: Y is being_plane and A3: X c= Y and A4: a = LDir X and A5: A = [(PDir Y),2] ; ::_thesis: a on A X '||' Y by A1, A2, A3, AFF_4:42; hence a on A by A1, A2, A4, A5, Th29; ::_thesis: verum end; 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 proof let AS be AffinSpace; ::_thesis: 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 let Y, X, X9 be Subset of AS; ::_thesis: 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 let a be POINT of (IncProjSp_of AS); ::_thesis: 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 let A be LINE of (IncProjSp_of AS); ::_thesis: ( Y is being_plane & X c= Y & X9 // X & a = LDir X9 & A = [(PDir Y),2] implies a on A ) assume that A1: Y is being_plane and A2: X c= Y and A3: X9 // X and A4: a = LDir X9 and A5: A = [(PDir Y),2] ; ::_thesis: a on A X is being_line by A3, AFF_1:36; then A6: X9 '||' Y by A1, A2, A3, AFF_4:42, AFF_4:56; X9 is being_line by A3, AFF_1:36; hence a on A by A1, A4, A5, A6, Th29; ::_thesis: verum end; 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 proof let AS be AffinSpace; ::_thesis: 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 let X be Subset of AS; ::_thesis: 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 let p be POINT of (IncProjSp_of AS); ::_thesis: 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 let A be LINE of (IncProjSp_of AS); ::_thesis: ( A = [X,1] & X is being_line & p on A & p is not Element of AS implies p = LDir X ) assume that A1: A = [X,1] and A2: X is being_line and A3: p on A and A4: p is not Element of AS ; ::_thesis: p = LDir X consider Xp being Subset of AS such that A5: p = LDir Xp and A6: Xp is being_line by A4, Th20; Xp '||' X by A1, A2, A3, A5, A6, Th28; hence p = LDir X by A2, A5, A6, Th12; ::_thesis: verum end; 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 proof let AS be AffinSpace; ::_thesis: 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 let X be Subset of AS; ::_thesis: 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 let p, a be POINT of (IncProjSp_of AS); ::_thesis: 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 let A be LINE of (IncProjSp_of AS); ::_thesis: ( A = [X,1] & X is being_line & p on A & a on A & a <> p & p is not Element of AS implies a is Element of AS ) assume that A1: A = [X,1] and A2: X is being_line and A3: p on A and A4: a on A and A5: a <> p and A6: p is not Element of AS ; ::_thesis: a is Element of AS assume a is not Element of AS ; ::_thesis: contradiction then a = LDir X by A1, A2, A4, Th34; hence contradiction by A1, A2, A3, A5, A6, Th34; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let X, Y be Subset of AS; ::_thesis: 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 ) let a be Element of the Points of (ProjHorizon AS); ::_thesis: 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 ) let A be Element of the Lines of (ProjHorizon AS); ::_thesis: ( a = LDir X & A = PDir Y & X is being_line & Y is being_plane implies ( a on A iff X '||' Y ) ) assume that A1: a = LDir X and A2: A = PDir Y and A3: X is being_line and A4: Y is being_plane ; ::_thesis: ( a on A iff X '||' Y ) A5: now__::_thesis:_(_a_on_A_implies_X_'||'_Y_) assume a on A ; ::_thesis: X '||' Y then [a,A] in the Inc of (ProjHorizon AS) by INCSP_1:def_1; then consider X9, Y9 being Subset of AS such that A6: a = LDir X9 and A7: A = PDir Y9 and A8: X9 is being_line and A9: Y9 is being_plane and A10: X9 '||' Y9 by Def12; X // X9 by A1, A3, A6, A8, Th11; then A11: X '||' Y9 by A10, AFF_4:56; Y9 '||' Y by A2, A4, A7, A9, Th13; hence X '||' Y by A9, A11, AFF_4:59, AFF_4:60; ::_thesis: verum end; now__::_thesis:_(_X_'||'_Y_implies_a_on_A_) assume X '||' Y ; ::_thesis: a on A then [a,A] in Inc_of_Dir AS by A1, A2, A3, A4, Def12; hence a on A by INCSP_1:def_1; ::_thesis: verum end; hence ( a on A iff X '||' Y ) by A5; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let a be Element of the Points of (ProjHorizon AS); ::_thesis: 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 ) let a9 be Element of the Points of (IncProjSp_of AS); ::_thesis: 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 ) let A be Element of the Lines of (ProjHorizon AS); ::_thesis: for A9 being LINE of (IncProjSp_of AS) st a9 = a & A9 = [A,2] holds ( a on A iff a9 on A9 ) let A9 be LINE of (IncProjSp_of AS); ::_thesis: ( a9 = a & A9 = [A,2] implies ( a on A iff a9 on A9 ) ) assume that A1: a9 = a and A2: A9 = [A,2] ; ::_thesis: ( a on A iff a9 on A9 ) consider X being Subset of AS such that A3: a = LDir X and A4: X is being_line by Th14; consider Y being Subset of AS such that A5: A = PDir Y and A6: Y is being_plane by Th15; A7: now__::_thesis:_(_a9_on_A9_implies_a_on_A_) assume a9 on A9 ; ::_thesis: a on A then X '||' Y by A1, A2, A3, A4, A5, A6, Th29; hence a on A by A3, A4, A5, A6, Th36; ::_thesis: verum end; now__::_thesis:_(_a_on_A_implies_a9_on_A9_) assume a on A ; ::_thesis: a9 on A9 then X '||' Y by A3, A4, A5, A6, Th36; hence a9 on A9 by A1, A2, A3, A4, A5, A6, Th29; ::_thesis: verum end; hence ( a on A iff a9 on A9 ) by A7; ::_thesis: verum end; 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 proof let AS be AffinSpace; ::_thesis: 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 let a, b be Element of the Points of (ProjHorizon AS); ::_thesis: 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 let A, K be Element of the Lines of (ProjHorizon AS); ::_thesis: ( a on A & a on K & b on A & b on K & not a = b implies A = K ) assume that A1: a on A and A2: a on K and A3: b on A and A4: b on K ; ::_thesis: ( a = b or A = K ) consider Y9 being Subset of AS such that A5: b = LDir Y9 and A6: Y9 is being_line by Th14; consider X9 being Subset of AS such that A7: K = PDir X9 and A8: X9 is being_plane by Th15; A9: Y9 '||' X9 by A4, A5, A6, A7, A8, Th36; consider Y being Subset of AS such that A10: a = LDir Y and A11: Y is being_line by Th14; assume a <> b ; ::_thesis: A = K then A12: not Y // Y9 by A10, A11, A5, A6, Th11; consider X being Subset of AS such that A13: A = PDir X and A14: X is being_plane by Th15; A15: Y9 '||' X by A3, A5, A6, A13, A14, Th36; A16: Y '||' X9 by A2, A10, A11, A7, A8, Th36; Y '||' X by A1, A10, A11, A13, A14, Th36; then X '||' X9 by A11, A6, A14, A8, A12, A16, A15, A9, Th5; hence A = K by A13, A14, A7, A8, Th13; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let A be Element of the Lines of (ProjHorizon AS); ::_thesis: 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 ) consider X being Subset of AS such that A1: A = PDir X and A2: X is being_plane by Th15; consider x, y, z being Element of AS such that A3: x in X and A4: y in X and A5: z in X and A6: not LIN x,y,z by A2, AFF_4:34; A7: y <> z by A6, AFF_1:7; then A8: Line (y,z) is being_line by AFF_1:def_3; then A9: Line (y,z) '||' X by A2, A4, A5, A7, AFF_4:19, AFF_4:42; A10: z <> x by A6, AFF_1:7; then A11: Line (x,z) is being_line by AFF_1:def_3; then A12: Line (x,z) '||' X by A2, A3, A5, A10, AFF_4:19, AFF_4:42; A13: x <> y by A6, AFF_1:7; then A14: Line (x,y) is being_line by AFF_1:def_3; then reconsider a = LDir (Line (x,y)), b = LDir (Line (y,z)), c = LDir (Line (x,z)) as Element of the Points of (ProjHorizon AS) by A8, A11, Th14; take a ; ::_thesis: ex 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 ) take b ; ::_thesis: ex 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 ) take c ; ::_thesis: ( a on A & b on A & c on A & a <> b & b <> c & c <> a ) Line (x,y) '||' X by A2, A3, A4, A13, A14, AFF_4:19, AFF_4:42; hence ( a on A & b on A & c on A ) by A1, A2, A14, A8, A11, A9, A12, Th36; ::_thesis: ( a <> b & b <> c & c <> a ) A15: x in Line (x,y) by AFF_1:15; A16: z in Line (y,z) by AFF_1:15; A17: y in Line (x,y) by AFF_1:15; A18: y in Line (y,z) by AFF_1:15; thus a <> b ::_thesis: ( b <> c & c <> a ) proof assume not a <> b ; ::_thesis: contradiction then Line (x,y) // Line (y,z) by A14, A8, Th11; then z in Line (x,y) by A17, A18, A16, AFF_1:45; hence contradiction by A6, A14, A15, A17, AFF_1:21; ::_thesis: verum end; A19: z in Line (x,z) by AFF_1:15; A20: x in Line (x,z) by AFF_1:15; thus b <> c ::_thesis: c <> a proof assume not b <> c ; ::_thesis: contradiction then Line (y,z) // Line (x,z) by A8, A11, Th11; then x in Line (y,z) by A16, A20, A19, AFF_1:45; hence contradiction by A6, A8, A18, A16, AFF_1:21; ::_thesis: verum end; thus c <> a ::_thesis: verum proof assume not c <> a ; ::_thesis: contradiction then Line (x,y) // Line (x,z) by A14, A11, Th11; then z in Line (x,y) by A15, A20, A19, AFF_1:45; hence contradiction by A6, A14, A15, A17, AFF_1:21; ::_thesis: verum end; end; 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let a, b be Element of the Points of (ProjHorizon AS); ::_thesis: ex A being Element of the Lines of (ProjHorizon AS) st ( a on A & b on A ) consider X being Subset of AS such that A1: a = LDir X and A2: X is being_line by Th14; consider X9 being Subset of AS such that A3: b = LDir X9 and A4: X9 is being_line by Th14; consider x, y being Element of AS such that A5: x in X9 and y in X9 and x <> y by A4, AFF_1:19; A6: x in x * X by A2, AFF_4:def_3; x * X is being_line by A2, AFF_4:27; then consider Z being Subset of AS such that A7: X9 c= Z and A8: x * X c= Z and A9: Z is being_plane by A4, A5, A6, AFF_4:38; A10: X9 '||' Z by A4, A7, A9, AFF_4:42; reconsider A = PDir Z as Element of the Lines of (ProjHorizon AS) by A9, Th15; take A ; ::_thesis: ( a on A & b on A ) X // x * X by A2, AFF_4:def_3; then X '||' Z by A2, A8, A9, AFF_4:41; hence ( a on A & b on A ) by A1, A2, A3, A4, A9, A10, Th36; ::_thesis: verum end; 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 proof let AS be AffinSpace; ::_thesis: ( AS is not AffinPlane implies 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 ) set x = the Element of AS; consider X being Subset of AS such that A1: the Element of AS in X and the Element of AS in X and the Element of AS in X and A2: X is being_plane by AFF_4:37; reconsider A = PDir X as Element of the Lines of (ProjHorizon AS) by A2, Th15; assume AS is not AffinPlane ; ::_thesis: not for a being Element of the Points of (ProjHorizon AS) for A being Element of the Lines of (ProjHorizon AS) holds a on A then consider t being Element of AS such that A3: not t in X by A2, AFF_4:48; set Y = Line ( the Element of AS,t); A4: Line ( the Element of AS,t) is being_line by A1, A3, AFF_1:def_3; then reconsider a = LDir (Line ( the Element of AS,t)) as Element of the Points of (ProjHorizon AS) by Th14; take a ; ::_thesis: not for A being Element of the Lines of (ProjHorizon AS) holds a on A take A ; ::_thesis: not a on A A5: t in Line ( the Element of AS,t) by AFF_1:15; A6: the Element of AS in Line ( the Element of AS,t) by AFF_1:15; thus not a on A ::_thesis: verum proof assume a on A ; ::_thesis: contradiction then Line ( the Element of AS,t) '||' X by A2, A4, Th36; then Line ( the Element of AS,t) c= X by A1, A2, A4, A6, AFF_4:43; hence contradiction by A3, A5; ::_thesis: verum end; end; 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 proof let AS be AffinSpace; ::_thesis: 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 let a, b be POINT of (IncProjSp_of AS); ::_thesis: 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 let A, K be LINE of (IncProjSp_of AS); ::_thesis: ( a on A & a on K & b on A & b on K & not a = b implies A = K ) assume that A1: a on A and A2: a on K and A3: b on A and A4: b on K ; ::_thesis: ( a = b or A = K ) consider X being Subset of AS such that A5: ( ( A = [X,1] & X is being_line ) or ( A = [(PDir X),2] & X is being_plane ) ) by Th23; consider X9 being Subset of AS such that A6: ( ( K = [X9,1] & X9 is being_line ) or ( K = [(PDir X9),2] & X9 is being_plane ) ) by Th23; assume A7: a <> b ; ::_thesis: A = K A8: now__::_thesis:_(_ex_Y_being_Subset_of_AS_st_ (_a_=_LDir_Y_&_Y_is_being_line_)_implies_A_=_K_) given Y being Subset of AS such that A9: a = LDir Y and A10: Y is being_line ; ::_thesis: A = K A11: now__::_thesis:_(_ex_Y9_being_Subset_of_AS_st_ (_b_=_LDir_Y9_&_Y9_is_being_line_)_implies_A_=_K_) given Y9 being Subset of AS such that A12: b = LDir Y9 and A13: Y9 is being_line ; ::_thesis: A = K A14: not Y // Y9 by A7, A9, A10, A12, A13, Th11; A15: for Z being Subset of AS for M being LINE of (IncProjSp_of AS) st M = [Z,1] & Z is being_line & a on M holds not b on M proof let Z be Subset of AS; ::_thesis: for M being LINE of (IncProjSp_of AS) st M = [Z,1] & Z is being_line & a on M holds not b on M let M be LINE of (IncProjSp_of AS); ::_thesis: ( M = [Z,1] & Z is being_line & a on M implies not b on M ) assume that A16: M = [Z,1] and A17: Z is being_line ; ::_thesis: ( not a on M or not b on M ) assume A18: ( a on M & b on M ) ; ::_thesis: contradiction then Y9 '||' Z by A12, A13, A16, A17, Th28; then A19: Y9 // Z by A13, A17, AFF_4:40; Y '||' Z by A9, A10, A16, A17, A18, Th28; then Y // Z by A10, A17, AFF_4:40; then Y // Y9 by A19, AFF_1:44; hence contradiction by A7, A9, A10, A12, A13, Th11; ::_thesis: verum end; then A20: Y9 '||' X by A1, A3, A5, A12, A13, Th29; A21: Y9 '||' X9 by A2, A4, A6, A12, A13, A15, Th29; A22: Y '||' X9 by A2, A4, A6, A9, A10, A15, Th29; Y '||' X by A1, A3, A5, A9, A10, A15, Th29; then X '||' X9 by A1, A2, A3, A4, A5, A6, A10, A13, A15, A14, A22, A20, A21, Th5; hence A = K by A1, A2, A3, A4, A5, A6, A15, Th13; ::_thesis: verum end; now__::_thesis:_(_b_is_Element_of_AS_implies_A_=_K_) assume b is Element of AS ; ::_thesis: A = K then reconsider y = b as Element of AS ; A23: y in X9 by A4, A6, Th26, Th27; A24: y = b ; then Y '||' X9 by A2, A4, A6, A9, A10, Th27, Th28; then A25: Y // X9 by A4, A6, A10, A24, Th27, AFF_4:40; Y '||' X by A1, A3, A5, A9, A10, A24, Th27, Th28; then Y // X by A3, A5, A10, A24, Th27, AFF_4:40; then A26: X // X9 by A25, AFF_1:44; y in X by A3, A5, Th26, Th27; hence A = K by A3, A4, A5, A6, A23, A26, Th27, AFF_1:45; ::_thesis: verum end; hence A = K by A11, Th20; ::_thesis: verum end; now__::_thesis:_(_a_is_Element_of_AS_implies_A_=_K_) assume a is Element of AS ; ::_thesis: A = K then reconsider x = a as Element of AS ; A27: x = a ; A28: x in X9 by A2, A6, Th26, Th27; A29: x in X by A1, A5, Th26, Th27; A30: now__::_thesis:_(_ex_Y_being_Subset_of_AS_st_ (_b_=_LDir_Y_&_Y_is_being_line_)_implies_A_=_K_) given Y being Subset of AS such that A31: b = LDir Y and A32: Y is being_line ; ::_thesis: A = K Y '||' X9 by A2, A4, A6, A27, A31, A32, Th27, Th28; then A33: Y // X9 by A2, A6, A27, A32, Th27, AFF_4:40; Y '||' X by A1, A3, A5, A27, A31, A32, Th27, Th28; then Y // X by A1, A5, A27, A32, Th27, AFF_4:40; then X // X9 by A33, AFF_1:44; hence A = K by A1, A2, A5, A6, A29, A28, Th27, AFF_1:45; ::_thesis: verum end; now__::_thesis:_(_b_is_Element_of_AS_implies_A_=_K_) assume b is Element of AS ; ::_thesis: A = K then reconsider y = b as Element of AS ; A34: y in X9 by A4, A6, Th26, Th27; y in X by A3, A5, Th26, Th27; hence A = K by A1, A2, A7, A5, A6, A29, A28, A34, Th27, AFF_1:18; ::_thesis: verum end; hence A = K by A30, Th20; ::_thesis: verum end; hence A = K by A8, Th20; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let A be LINE of (IncProjSp_of AS); ::_thesis: 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 ) consider X being Subset of AS such that A1: ( ( A = [X,1] & X is being_line ) or ( A = [(PDir X),2] & X is being_plane ) ) by Th23; A2: now__::_thesis:_(_A_=_[(PDir_X),2]_&_X_is_being_plane_implies_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_)_) assume that A3: A = [(PDir X),2] and A4: X is being_plane ; ::_thesis: 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 ) consider x, y, z being Element of AS such that A5: x in X and A6: y in X and A7: z in X and A8: not LIN x,y,z by A4, AFF_4:34; A9: y <> z by A8, AFF_1:7; then A10: Line (y,z) is being_line by AFF_1:def_3; then A11: Line (y,z) '||' X by A4, A6, A7, A9, AFF_4:19, AFF_4:42; A12: z <> x by A8, AFF_1:7; then A13: Line (x,z) is being_line by AFF_1:def_3; then A14: Line (x,z) '||' X by A4, A5, A7, A12, AFF_4:19, AFF_4:42; A15: x <> y by A8, AFF_1:7; then A16: Line (x,y) is being_line by AFF_1:def_3; then reconsider a = LDir (Line (x,y)), b = LDir (Line (y,z)), c = LDir (Line (x,z)) as POINT of (IncProjSp_of AS) by A10, A13, Th20; take a = a; ::_thesis: ex b, c being POINT of (IncProjSp_of AS) st ( a on A & b on A & c on A & a <> b & b <> c & c <> a ) take b = b; ::_thesis: ex c being POINT of (IncProjSp_of AS) st ( a on A & b on A & c on A & a <> b & b <> c & c <> a ) take c = c; ::_thesis: ( a on A & b on A & c on A & a <> b & b <> c & c <> a ) Line (x,y) '||' X by A4, A5, A6, A15, A16, AFF_4:19, AFF_4:42; hence ( a on A & b on A & c on A ) by A3, A4, A16, A10, A13, A11, A14, Th29; ::_thesis: ( a <> b & b <> c & c <> a ) A17: x in Line (x,y) by AFF_1:15; A18: z in Line (y,z) by AFF_1:15; A19: y in Line (x,y) by AFF_1:15; A20: y in Line (y,z) by AFF_1:15; thus a <> b ::_thesis: ( b <> c & c <> a ) proof assume not a <> b ; ::_thesis: contradiction then Line (x,y) // Line (y,z) by A16, A10, Th11; then z in Line (x,y) by A19, A20, A18, AFF_1:45; hence contradiction by A8, A16, A17, A19, AFF_1:21; ::_thesis: verum end; A21: z in Line (x,z) by AFF_1:15; A22: x in Line (x,z) by AFF_1:15; thus b <> c ::_thesis: c <> a proof assume not b <> c ; ::_thesis: contradiction then Line (y,z) // Line (x,z) by A10, A13, Th11; then x in Line (y,z) by A18, A22, A21, AFF_1:45; hence contradiction by A8, A10, A20, A18, AFF_1:21; ::_thesis: verum end; thus c <> a ::_thesis: verum proof assume not c <> a ; ::_thesis: contradiction then Line (x,y) // Line (x,z) by A16, A13, Th11; then z in Line (x,y) by A17, A22, A21, AFF_1:45; hence contradiction by A8, A16, A17, A19, AFF_1:21; ::_thesis: verum end; end; now__::_thesis:_(_A_=_[X,1]_&_X_is_being_line_implies_ex_a,_b_being_Element_of_the_Points_of_(IncProjSp_of_AS)_ex_c_being_POINT_of_(IncProjSp_of_AS)_st_ (_a_on_A_&_b_on_A_&_c_on_A_&_a_<>_b_&_b_<>_c_&_c_<>_a_)_) assume that A23: A = [X,1] and A24: X is being_line ; ::_thesis: ex a, b being Element of the Points of (IncProjSp_of AS) ex c being POINT of (IncProjSp_of AS) st ( a on A & b on A & c on A & a <> b & b <> c & c <> a ) reconsider c = LDir X as POINT of (IncProjSp_of AS) by A24, Th20; consider x, y being Element of AS such that A25: x in X and A26: y in X and A27: x <> y by A24, AFF_1:19; reconsider a = x, b = y as Element of the Points of (IncProjSp_of AS) by Th20; take a = a; ::_thesis: ex b being Element of the Points of (IncProjSp_of AS) ex c being POINT of (IncProjSp_of AS) st ( a on A & b on A & c on A & a <> b & b <> c & c <> a ) take b = b; ::_thesis: ex c being POINT of (IncProjSp_of AS) st ( a on A & b on A & c on A & a <> b & b <> c & c <> a ) take c = c; ::_thesis: ( a on A & b on A & c on A & a <> b & b <> c & c <> a ) X // X by A24, AFF_1:41; then X '||' X by A24, AFF_4:40; hence ( a on A & b on A & c on A ) by A23, A24, A25, A26, Th26, Th28; ::_thesis: ( a <> b & b <> c & c <> a ) thus a <> b by A27; ::_thesis: ( b <> c & c <> a ) thus ( b <> c & c <> a ) ::_thesis: verum proof assume A28: ( not b <> c or not c <> a ) ; ::_thesis: contradiction c in Dir_of_Lines AS by A24, Th14; then the carrier of AS /\ (Dir_of_Lines AS) <> {} by A28, XBOOLE_0:def_4; then the carrier of AS meets Dir_of_Lines AS by XBOOLE_0:def_7; hence contradiction by Th16; ::_thesis: verum end; end; hence 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 ) by A1, A2; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: for a, b being POINT of (IncProjSp_of AS) ex A being LINE of (IncProjSp_of AS) st ( a on A & b on A ) let a, b be POINT of (IncProjSp_of AS); ::_thesis: ex A being LINE of (IncProjSp_of AS) st ( a on A & b on A ) A1: now__::_thesis:_(_ex_X_being_Subset_of_AS_st_ (_a_=_LDir_X_&_X_is_being_line_)_implies_ex_A_being_LINE_of_(IncProjSp_of_AS)_st_ (_a_on_A_&_b_on_A_)_) given X being Subset of AS such that A2: a = LDir X and A3: X is being_line ; ::_thesis: ex A being LINE of (IncProjSp_of AS) st ( a on A & b on A ) A4: now__::_thesis:_(_ex_X9_being_Subset_of_AS_st_ (_b_=_LDir_X9_&_X9_is_being_line_)_implies_ex_A_being_LINE_of_(IncProjSp_of_AS)_st_ (_a_on_A_&_b_on_A_)_) given X9 being Subset of AS such that A5: b = LDir X9 and A6: X9 is being_line ; ::_thesis: ex A being LINE of (IncProjSp_of AS) st ( a on A & b on A ) consider x, y being Element of AS such that A7: x in X9 and y in X9 and x <> y by A6, AFF_1:19; A8: x in x * X by A3, AFF_4:def_3; x * X is being_line by A3, AFF_4:27; then consider Z being Subset of AS such that A9: X9 c= Z and A10: x * X c= Z and A11: Z is being_plane by A6, A7, A8, AFF_4:38; A12: X9 '||' Z by A6, A9, A11, AFF_4:42; reconsider A = [(PDir Z),2] as LINE of (IncProjSp_of AS) by A11, Th23; take A = A; ::_thesis: ( a on A & b on A ) X // x * X by A3, AFF_4:def_3; then X '||' Z by A3, A10, A11, AFF_4:41; hence ( a on A & b on A ) by A2, A3, A5, A6, A11, A12, Th29; ::_thesis: verum end; now__::_thesis:_(_b_is_Element_of_AS_implies_ex_A_being_LINE_of_(IncProjSp_of_AS)_st_ (_a_on_A_&_b_on_A_)_) assume b is Element of AS ; ::_thesis: ex A being LINE of (IncProjSp_of AS) st ( a on A & b on A ) then reconsider y = b as Element of AS ; A13: y * X is being_line by A3, AFF_4:27; then reconsider A = [(y * X),1] as LINE of (IncProjSp_of AS) by Th23; take A = A; ::_thesis: ( a on A & b on A ) X // y * X by A3, AFF_4:def_3; then X '||' y * X by A3, A13, AFF_4:40; hence a on A by A2, A3, A13, Th28; ::_thesis: b on A y in y * X by A3, AFF_4:def_3; hence b on A by A13, Th26; ::_thesis: verum end; hence ex A being LINE of (IncProjSp_of AS) st ( a on A & b on A ) by A4, Th20; ::_thesis: verum end; now__::_thesis:_(_a_is_Element_of_AS_implies_ex_A_being_LINE_of_(IncProjSp_of_AS)_st_ (_a_on_A_&_b_on_A_)_) assume a is Element of AS ; ::_thesis: ex A being LINE of (IncProjSp_of AS) st ( a on A & b on A ) then reconsider x = a as Element of AS ; A14: now__::_thesis:_(_ex_X9_being_Subset_of_AS_st_ (_b_=_LDir_X9_&_X9_is_being_line_)_implies_ex_A_being_LINE_of_(IncProjSp_of_AS)_st_ (_a_on_A_&_b_on_A_)_) given X9 being Subset of AS such that A15: b = LDir X9 and A16: X9 is being_line ; ::_thesis: ex A being LINE of (IncProjSp_of AS) st ( a on A & b on A ) A17: x * X9 is being_line by A16, AFF_4:27; then reconsider A = [(x * X9),1] as LINE of (IncProjSp_of AS) by Th23; take A = A; ::_thesis: ( a on A & b on A ) x in x * X9 by A16, AFF_4:def_3; hence a on A by A17, Th26; ::_thesis: b on A X9 // x * X9 by A16, AFF_4:def_3; then X9 '||' x * X9 by A16, A17, AFF_4:40; hence b on A by A15, A16, A17, Th28; ::_thesis: verum end; now__::_thesis:_(_b_is_Element_of_AS_implies_ex_A_being_LINE_of_(IncProjSp_of_AS)_st_ (_a_on_A_&_b_on_A_)_) assume b is Element of AS ; ::_thesis: ex A being LINE of (IncProjSp_of AS) st ( a on A & b on A ) then reconsider y = b as Element of AS ; consider Y being Subset of AS such that A18: x in Y and A19: y in Y and A20: Y is being_line by AFF_4:11; reconsider A = [Y,1] as LINE of (IncProjSp_of AS) by A20, Th23; take A = A; ::_thesis: ( a on A & b on A ) thus ( a on A & b on A ) by A18, A19, A20, Th26; ::_thesis: verum end; hence ex A being LINE of (IncProjSp_of AS) st ( a on A & b on A ) by A14, Th20; ::_thesis: verum end; hence ex A being LINE of (IncProjSp_of AS) st ( a on A & b on A ) by A1, Th20; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let A, K be LINE of (IncProjSp_of AS); ::_thesis: ( AS is AffinPlane implies ex a being POINT of (IncProjSp_of AS) st ( a on A & a on K ) ) consider X being Subset of AS such that A1: ( ( A = [X,1] & X is being_line ) or ( A = [(PDir X),2] & X is being_plane ) ) by Th23; consider X9 being Subset of AS such that A2: ( ( K = [X9,1] & X9 is being_line ) or ( K = [(PDir X9),2] & X9 is being_plane ) ) by Th23; assume A3: AS is AffinPlane ; ::_thesis: ex a being POINT of (IncProjSp_of AS) st ( a on A & a on K ) A4: now__::_thesis:_(_A_=_[X,1]_&_X_is_being_line_implies_ex_a_being_POINT_of_(IncProjSp_of_AS)_st_ (_a_on_A_&_a_on_K_)_) assume that A5: A = [X,1] and A6: X is being_line ; ::_thesis: ex a being POINT of (IncProjSp_of AS) st ( a on A & a on K ) A7: now__::_thesis:_(_K_=_[X9,1]_&_X9_is_being_line_implies_ex_a_being_POINT_of_(IncProjSp_of_AS)_st_ (_a_on_A_&_a_on_K_)_) assume that A8: K = [X9,1] and A9: X9 is being_line ; ::_thesis: ex a being POINT of (IncProjSp_of AS) st ( a on A & a on K ) A10: now__::_thesis:_(_X_//_X9_implies_ex_a_being_Element_of_the_Points_of_(IncProjSp_of_AS)_st_ (_a_on_A_&_a_on_K_)_) reconsider a = LDir X, b = LDir X9 as Element of the Points of (IncProjSp_of AS) by A6, A9, Th20; X9 // X9 by A9, AFF_1:41; then A11: X9 '||' X9 by A9, AFF_4:40; assume X // X9 ; ::_thesis: ex a being Element of the Points of (IncProjSp_of AS) st ( a on A & a on K ) then A12: a = b by A6, A9, Th11; take a = a; ::_thesis: ( a on A & a on K ) X // X by A6, AFF_1:41; then X '||' X by A6, AFF_4:40; hence ( a on A & a on K ) by A5, A6, A8, A9, A12, A11, Th28; ::_thesis: verum end; now__::_thesis:_(_not_X_//_X9_implies_ex_a_being_Element_of_the_Points_of_(IncProjSp_of_AS)_st_ (_a_on_A_&_a_on_K_)_) assume not X // X9 ; ::_thesis: ex a being Element of the Points of (IncProjSp_of AS) st ( a on A & a on K ) then consider x being Element of AS such that A13: x in X and A14: x in X9 by A3, A6, A9, AFF_1:58; reconsider a = x as Element of the Points of (IncProjSp_of AS) by Th20; take a = a; ::_thesis: ( a on A & a on K ) thus ( a on A & a on K ) by A5, A6, A8, A9, A13, A14, Th26; ::_thesis: verum end; hence ex a being POINT of (IncProjSp_of AS) st ( a on A & a on K ) by A10; ::_thesis: verum end; now__::_thesis:_(_K_=_[(PDir_X9),2]_&_X9_is_being_plane_implies_ex_a_being_Element_of_the_Points_of_(IncProjSp_of_AS)_st_ (_a_on_A_&_a_on_K_)_) X // X by A6, AFF_1:41; then A15: X '||' X by A6, AFF_4:40; reconsider a = LDir X as Element of the Points of (IncProjSp_of AS) by A6, Th20; assume that A16: K = [(PDir X9),2] and A17: X9 is being_plane ; ::_thesis: ex a being Element of the Points of (IncProjSp_of AS) st ( a on A & a on K ) take a = a; ::_thesis: ( a on A & a on K ) X9 = the carrier of AS by A3, A17, Th2; then X '||' X9 by A6, A17, AFF_4:42; hence ( a on A & a on K ) by A5, A6, A16, A17, A15, Th28, Th29; ::_thesis: verum end; hence ex a being POINT of (IncProjSp_of AS) st ( a on A & a on K ) by A2, A7; ::_thesis: verum end; now__::_thesis:_(_A_=_[(PDir_X),2]_&_X_is_being_plane_implies_ex_a_being_POINT_of_(IncProjSp_of_AS)_st_ (_a_on_A_&_a_on_K_)_) assume that A18: A = [(PDir X),2] and A19: X is being_plane ; ::_thesis: ex a being POINT of (IncProjSp_of AS) st ( a on A & a on K ) A20: X = the carrier of AS by A3, A19, Th2; A21: now__::_thesis:_(_K_=_[X9,1]_&_X9_is_being_line_implies_ex_a_being_POINT_of_(IncProjSp_of_AS)_st_ (_a_on_A_&_a_on_K_)_) assume that A22: K = [X9,1] and A23: X9 is being_line ; ::_thesis: ex a being POINT of (IncProjSp_of AS) st ( a on A & a on K ) X9 // X9 by A23, AFF_1:41; then A24: X9 '||' X9 by A23, AFF_4:40; reconsider a = LDir X9 as POINT of (IncProjSp_of AS) by A23, Th20; take a = a; ::_thesis: ( a on A & a on K ) X9 '||' X by A19, A20, A23, AFF_4:42; hence ( a on A & a on K ) by A18, A19, A22, A23, A24, Th28, Th29; ::_thesis: verum end; now__::_thesis:_(_K_=_[(PDir_X9),2]_&_X9_is_being_plane_implies_ex_a_being_POINT_of_(IncProjSp_of_AS)_st_ (_a_on_A_&_a_on_K_)_) consider a, b, c being POINT of (IncProjSp_of AS) such that A25: a on A and b on A and c on A and a <> b and b <> c and c <> a by Lm3; assume that A26: K = [(PDir X9),2] and A27: X9 is being_plane ; ::_thesis: ex a being POINT of (IncProjSp_of AS) st ( a on A & a on K ) take a = a; ::_thesis: ( a on A & a on K ) thus ( a on A & a on K ) by A3, A18, A19, A26, A27, A25, Th3; ::_thesis: verum end; hence ex a being POINT of (IncProjSp_of AS) st ( a on A & a on K ) by A2, A21; ::_thesis: verum end; hence ex a being POINT of (IncProjSp_of AS) st ( a on A & a on K ) by A1, A4; ::_thesis: verum end; 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 proof let AS be AffinSpace; ::_thesis: not for a being POINT of (IncProjSp_of AS) for A being LINE of (IncProjSp_of AS) holds a on A consider x, y, z being Element of AS such that A1: not LIN x,y,z by AFF_1:12; y <> z by A1, AFF_1:7; then A2: Line (y,z) is being_line by AFF_1:def_3; then reconsider A = [(Line (y,z)),1] as LINE of (IncProjSp_of AS) by Th23; reconsider a = x as POINT of (IncProjSp_of AS) by Th20; take a ; ::_thesis: not for A being LINE of (IncProjSp_of AS) holds a on A take A ; ::_thesis: not a on A thus not a on A ::_thesis: verum proof assume a on A ; ::_thesis: contradiction then A3: x in Line (y,z) by Th26; A4: z in Line (y,z) by AFF_1:15; y in Line (y,z) by AFF_1:15; hence contradiction by A1, A2, A3, A4, AFF_1:21; ::_thesis: verum end; end; 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] proof let AS be AffinSpace; ::_thesis: 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] let x, y be Element of the Points of (ProjHorizon AS); ::_thesis: 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] let X be Element of the Lines of (IncProjSp_of AS); ::_thesis: ( x <> y & [x,X] in the Inc of (IncProjSp_of AS) & [y,X] in the Inc of (IncProjSp_of AS) implies ex Y being Element of the Lines of (ProjHorizon AS) st X = [Y,2] ) reconsider a = x, b = y as POINT of (IncProjSp_of AS) by Th22; assume that A1: x <> y and A2: [x,X] in the Inc of (IncProjSp_of AS) and A3: [y,X] in the Inc of (IncProjSp_of AS) ; ::_thesis: ex Y being Element of the Lines of (ProjHorizon AS) st X = [Y,2] A4: b on X by A3, INCSP_1:def_1; consider Y being Element of the Lines of (ProjHorizon AS) such that A5: x on Y and A6: y on Y by Th40; reconsider A = [Y,2] as LINE of (IncProjSp_of AS) by Th25; consider Z being Subset of AS such that A7: Y = PDir Z and A8: Z is being_plane by Th15; consider X2 being Subset of AS such that A9: y = LDir X2 and A10: X2 is being_line by Th14; X2 '||' Z by A9, A10, A6, A7, A8, Th36; then A11: b on A by A9, A10, A7, A8, Th29; take Y ; ::_thesis: X = [Y,2] consider X1 being Subset of AS such that A12: x = LDir X1 and A13: X1 is being_line by Th14; X1 '||' Z by A12, A13, A5, A7, A8, Th36; then A14: a on A by A12, A13, A7, A8, Th29; a on X by A2, INCSP_1:def_1; hence X = [Y,2] by A1, A4, A14, A11, Lm2; ::_thesis: verum end; 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) proof let AS be AffinSpace; ::_thesis: 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) let x be POINT of (IncProjSp_of AS); ::_thesis: 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) let X be Element of the Lines of (ProjHorizon AS); ::_thesis: ( [x,[X,2]] in the Inc of (IncProjSp_of AS) implies x is Element of the Points of (ProjHorizon AS) ) assume A1: [x,[X,2]] in the Inc of (IncProjSp_of AS) ; ::_thesis: x is Element of the Points of (ProjHorizon AS) reconsider A = [X,2] as LINE of (IncProjSp_of AS) by Th25; A2: ex Y being Subset of AS st ( X = PDir Y & Y is being_plane ) by Th15; x is not Element of AS proof assume x is Element of AS ; ::_thesis: contradiction then reconsider a = x as Element of AS ; A3: a = x ; x on A by A1, INCSP_1:def_1; hence contradiction by A2, A3, Th27; ::_thesis: verum end; then ex Y9 being Subset of AS st ( x = LDir Y9 & Y9 is being_line ) by Th20; hence x is Element of the Points of (ProjHorizon AS) by Th14; ::_thesis: verum end; 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 proof let AS be AffinSpace; ::_thesis: 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 let X, X9, Y, Y9 be Subset of AS; ::_thesis: 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 let b, c be POINT of (IncProjSp_of AS); ::_thesis: 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 let A, K, M be LINE of (IncProjSp_of AS); ::_thesis: ( 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 implies Y9 c= Y ) assume that A1: X is being_line and A2: X9 is being_line and A3: Y is being_plane and A4: X c= Y and A5: X9 c= Y and A6: A = [X,1] and A7: K = [X9,1] and A8: b on A and A9: c on K and A10: b on M and A11: c on M and A12: b <> c and A13: M = [Y9,1] and A14: Y9 is being_line ; ::_thesis: Y9 c= Y A15: now__::_thesis:_(_b_is_Element_of_AS_implies_Y9_c=_Y_) assume b is Element of AS ; ::_thesis: Y9 c= Y then reconsider y = b as Element of AS ; A16: now__::_thesis:_(_ex_Xc_being_Subset_of_AS_st_ (_c_=_LDir_Xc_&_Xc_is_being_line_)_implies_Y9_c=_Y_) given Xc being Subset of AS such that A17: c = LDir Xc and A18: Xc is being_line ; ::_thesis: Y9 c= Y Xc '||' X9 by A2, A7, A9, A17, A18, Th28; then A19: Xc // X9 by A2, A18, AFF_4:40; Xc '||' Y9 by A11, A13, A14, A17, A18, Th28; then Xc // Y9 by A14, A18, AFF_4:40; then A20: X9 // Y9 by A19, AFF_1:44; y in Y9 by A10, A13, Th26; then A21: Y9 = y * X9 by A2, A20, AFF_4:def_3; y in X by A6, A8, Th26; hence Y9 c= Y by A2, A3, A4, A5, A21, AFF_4:28; ::_thesis: verum end; now__::_thesis:_(_c_is_Element_of_AS_implies_Y9_c=_Y_) assume c is Element of AS ; ::_thesis: Y9 c= Y then reconsider z = c as Element of AS ; A22: z in Y9 by A11, A13, Th26; y in Y9 by A10, A13, Th26; then A23: Y9 = Line (y,z) by A12, A14, A22, AFF_1:57; A24: z in X9 by A7, A9, Th26; y in X by A6, A8, Th26; hence Y9 c= Y by A3, A4, A5, A12, A24, A23, AFF_4:19; ::_thesis: verum end; hence Y9 c= Y by A16, Th20; ::_thesis: verum end; now__::_thesis:_(_ex_Xb_being_Subset_of_AS_st_ (_b_=_LDir_Xb_&_Xb_is_being_line_)_implies_Y9_c=_Y_) given Xb being Subset of AS such that A25: b = LDir Xb and A26: Xb is being_line ; ::_thesis: Y9 c= Y A27: now__::_thesis:_(_c_is_Element_of_AS_implies_Y9_c=_Y_) assume c is Element of AS ; ::_thesis: Y9 c= Y then reconsider y = c as Element of AS ; Xb '||' X by A1, A6, A8, A25, A26, Th28; then A28: Xb // X by A1, A26, AFF_4:40; Xb '||' Y9 by A10, A13, A14, A25, A26, Th28; then Xb // Y9 by A14, A26, AFF_4:40; then A29: X // Y9 by A28, AFF_1:44; y in Y9 by A11, A13, Th26; then A30: Y9 = y * X by A1, A29, AFF_4:def_3; y in X9 by A7, A9, Th26; hence Y9 c= Y by A1, A3, A4, A5, A30, AFF_4:28; ::_thesis: verum end; now__::_thesis:_for_Xc_being_Subset_of_AS_holds_ (_not_c_=_LDir_Xc_or_not_Xc_is_being_line_) Xb '||' Y9 by A10, A13, A14, A25, A26, Th28; then A31: Xb // Y9 by A14, A26, AFF_4:40; given Xc being Subset of AS such that A32: c = LDir Xc and A33: Xc is being_line ; ::_thesis: contradiction Xc '||' Y9 by A11, A13, A14, A32, A33, Th28; then Xc // Y9 by A14, A33, AFF_4:40; then Xc // Xb by A31, AFF_1:44; hence contradiction by A12, A25, A26, A32, A33, Th11; ::_thesis: verum end; hence Y9 c= Y by A27, Th20; ::_thesis: verum end; hence Y9 c= Y by A15, Th20; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let X, X9, Y, Y9 be Subset of AS; ::_thesis: 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 ) let b, c be POINT of (IncProjSp_of AS); ::_thesis: 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 ) let A, K, M be LINE of (IncProjSp_of AS); ::_thesis: ( 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 implies ( Y9 '||' Y & Y '||' Y9 ) ) assume that A1: X is being_line and A2: X9 is being_line and A3: Y is being_plane and A4: X c= Y and A5: X9 c= Y and A6: A = [X,1] and A7: K = [X9,1] and A8: b on A and A9: c on K and A10: b on M and A11: c on M and A12: b <> c and A13: M = [(PDir Y9),2] and A14: Y9 is being_plane ; ::_thesis: ( Y9 '||' Y & Y '||' Y9 ) ( b is Element of AS or ex Xb being Subset of AS st ( b = LDir Xb & Xb is being_line ) ) by Th20; then consider Xb being Subset of AS such that A15: b = LDir Xb and A16: Xb is being_line by A10, A13, Th27; A17: Xb '||' Y9 by A10, A13, A14, A15, A16, Th29; Xb '||' X by A1, A6, A8, A15, A16, Th28; then Xb // X by A1, A16, AFF_4:40; then A18: Xb '||' Y by A1, A3, A4, AFF_4:42, AFF_4:56; ( c is Element of AS or ex Xc being Subset of AS st ( c = LDir Xc & Xc is being_line ) ) by Th20; then consider Xc being Subset of AS such that A19: c = LDir Xc and A20: Xc is being_line by A11, A13, Th27; A21: Xc '||' Y9 by A11, A13, A14, A19, A20, Th29; Xc '||' X9 by A2, A7, A9, A19, A20, Th28; then Xc // X9 by A2, A20, AFF_4:40; then A22: Xc '||' Y by A2, A3, A5, AFF_4:42, AFF_4:56; not Xb // Xc by A12, A15, A16, A19, A20, Th11; hence ( Y9 '||' Y & Y '||' Y9 ) by A3, A14, A16, A20, A17, A21, A18, A22, Th5; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let Y, X, X9 be Subset of AS; ::_thesis: 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 ) let P, Q be LINE of (IncProjSp_of AS); ::_thesis: ( Y is being_plane & X is being_line & X9 is being_line & X c= Y & X9 c= Y & P = [X,1] & Q = [X9,1] implies ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) ) assume that A1: Y is being_plane and A2: X is being_line and A3: X9 is being_line and A4: X c= Y and A5: X9 c= Y and A6: P = [X,1] and A7: Q = [X9,1] ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) A8: now__::_thesis:_(_X_//_X9_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_ (_q_on_P_&_q_on_Q_)_) reconsider q = LDir X as POINT of (IncProjSp_of AS) by A2, Th20; assume A9: X // X9 ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) take q = q; ::_thesis: ( q on P & q on Q ) LDir X = LDir X9 by A2, A3, A9, Th11; hence ( q on P & q on Q ) by A2, A3, A6, A7, Th30; ::_thesis: verum end; now__::_thesis:_(_ex_y_being_Element_of_AS_st_ (_y_in_X_&_y_in_X9_)_implies_ex_q_being_Element_of_the_Points_of_(IncProjSp_of_AS)_st_ (_q_on_P_&_q_on_Q_)_) given y being Element of AS such that A10: y in X and A11: y in X9 ; ::_thesis: ex q being Element of the Points of (IncProjSp_of AS) st ( q on P & q on Q ) reconsider q = y as Element of the Points of (IncProjSp_of AS) by Th20; take q = q; ::_thesis: ( q on P & q on Q ) thus ( q on P & q on Q ) by A2, A3, A6, A7, A10, A11, Th26; ::_thesis: verum end; hence ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) by A1, A2, A3, A4, A5, A8, AFF_4:22; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let a, b, c, d, p be POINT of (IncProjSp_of AS); ::_thesis: 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 ) let M, N, P, Q be LINE of (IncProjSp_of AS); ::_thesis: ( 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 implies ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) ) assume that A1: a on M and A2: b on M and A3: c on N and A4: d on N and A5: p on M and A6: p on N and A7: a on P and A8: c on P and A9: b on Q and A10: d on Q and A11: not p on P and A12: not p on Q and A13: M <> N and A14: p is Element of AS ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) A15: b <> d by A2, A4, A5, A6, A9, A12, A13, Lm2; reconsider x = p as Element of AS by A14; consider XM being Subset of AS such that A16: ( ( M = [XM,1] & XM is being_line ) or ( M = [(PDir XM),2] & XM is being_plane ) ) by Th23; consider XQ being Subset of AS such that A17: ( ( Q = [XQ,1] & XQ is being_line ) or ( Q = [(PDir XQ),2] & XQ is being_plane ) ) by Th23; consider XP being Subset of AS such that A18: ( ( P = [XP,1] & XP is being_line ) or ( P = [(PDir XP),2] & XP is being_plane ) ) by Th23; consider XN being Subset of AS such that A19: ( ( N = [XN,1] & XN is being_line ) or ( N = [(PDir XN),2] & XN is being_plane ) ) by Th23; A20: x in XM by A5, A16, Th26, Th27; x in XN by A6, A19, Th26, Th27; then consider Y being Subset of AS such that A21: XM c= Y and A22: XN c= Y and A23: Y is being_plane by A5, A6, A16, A19, A20, Th27, AFF_4:38; A24: a <> c by A1, A3, A5, A6, A7, A11, A13, Lm2; A25: now__::_thesis:_(_P_=_[(PDir_XP),2]_&_XP_is_being_plane_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_ (_q_on_P_&_q_on_Q_)_) assume that A26: P = [(PDir XP),2] and A27: XP is being_plane ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) A28: Y '||' XP by A1, A3, A5, A6, A7, A8, A24, A16, A19, A20, A21, A22, A23, A26, A27, Lm8, Th27; A29: now__::_thesis:_(_Q_=_[XQ,1]_&_XQ_is_being_line_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_ (_q_on_P_&_q_on_Q_)_) assume that A30: Q = [XQ,1] and A31: XQ is being_line ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) reconsider q = LDir XQ as POINT of (IncProjSp_of AS) by A31, Th20; take q = q; ::_thesis: ( q on P & q on Q ) XQ c= Y by A2, A4, A5, A6, A9, A10, A15, A16, A19, A20, A21, A22, A23, A30, A31, Lm7, Th27; then XQ '||' Y by A23, A31, AFF_4:42; then XQ '||' XP by A23, A28, AFF_4:59, AFF_4:60; hence q on P by A26, A27, A31, Th29; ::_thesis: q on Q thus q on Q by A30, A31, Th30; ::_thesis: verum end; now__::_thesis:_(_Q_=_[(PDir_XQ),2]_&_XQ_is_being_plane_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_ (_q_on_P_&_q_on_Q_)_) consider q, r, p9 being POINT of (IncProjSp_of AS) such that A32: q on P and r on P and p9 on P and q <> r and r <> p9 and p9 <> q by Lm3; assume that A33: Q = [(PDir XQ),2] and A34: XQ is being_plane ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) take q = q; ::_thesis: ( q on P & q on Q ) thus q on P by A32; ::_thesis: q on Q Y '||' XQ by A2, A4, A5, A6, A9, A10, A15, A16, A19, A20, A21, A22, A23, A33, A34, Lm8, Th27; then XP '||' XQ by A23, A27, A28, A34, AFF_4:61; hence q on Q by A26, A27, A33, A34, A32, Th13; ::_thesis: verum end; hence ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) by A17, A29; ::_thesis: verum end; now__::_thesis:_(_P_=_[XP,1]_&_XP_is_being_line_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_ (_q_on_P_&_q_on_Q_)_) assume that A35: P = [XP,1] and A36: XP is being_line ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) A37: XP c= Y by A1, A3, A5, A6, A7, A8, A24, A16, A19, A20, A21, A22, A23, A35, A36, Lm7, Th27; A38: now__::_thesis:_(_Q_=_[(PDir_XQ),2]_&_XQ_is_being_plane_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_ (_q_on_P_&_q_on_Q_)_) A39: XP '||' Y by A23, A36, A37, AFF_4:42; reconsider q = LDir XP as POINT of (IncProjSp_of AS) by A36, Th20; assume that A40: Q = [(PDir XQ),2] and A41: XQ is being_plane ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) take q = q; ::_thesis: ( q on P & q on Q ) thus q on P by A35, A36, Th30; ::_thesis: q on Q Y '||' XQ by A2, A4, A5, A6, A9, A10, A15, A16, A19, A20, A21, A22, A23, A40, A41, Lm8, Th27; then XP '||' XQ by A23, A39, AFF_4:59, AFF_4:60; hence q on Q by A36, A40, A41, Th29; ::_thesis: verum end; now__::_thesis:_(_Q_=_[XQ,1]_&_XQ_is_being_line_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_ (_q_on_P_&_q_on_Q_)_) assume that A42: Q = [XQ,1] and A43: XQ is being_line ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) XQ c= Y by A2, A4, A5, A6, A9, A10, A15, A16, A19, A20, A21, A22, A23, A42, A43, Lm7, Th27; hence ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) by A23, A35, A36, A37, A42, A43, Th43; ::_thesis: verum end; hence ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) by A17, A38; ::_thesis: verum end; hence ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) by A18, A25; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let a, b, c, d, p be POINT of (IncProjSp_of AS); ::_thesis: 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 ) let M, N, P, Q be LINE of (IncProjSp_of AS); ::_thesis: ( 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 implies ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) ) assume that A1: a on M and A2: b on M and A3: c on N and A4: d on N and A5: p on M and A6: p on N and A7: a on P and A8: c on P and A9: b on Q and A10: d on Q and A11: not p on P and A12: not p on Q and A13: M <> N and A14: p is not Element of AS and A15: a is Element of AS ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) reconsider x = a as Element of AS by A15; consider XM being Subset of AS such that A16: ( ( M = [XM,1] & XM is being_line ) or ( M = [(PDir XM),2] & XM is being_plane ) ) by Th23; A17: x in XM by A1, A16, Th26, Th27; A18: b <> d by A2, A4, A5, A6, A9, A12, A13, Lm2; consider XN being Subset of AS such that A19: ( ( N = [XN,1] & XN is being_line ) or ( N = [(PDir XN),2] & XN is being_plane ) ) by Th23; consider XP being Subset of AS such that A20: ( ( P = [XP,1] & XP is being_line ) or ( P = [(PDir XP),2] & XP is being_plane ) ) by Th23; A21: x = a ; then reconsider y = b as Element of AS by A1, A2, A5, A9, A12, A14, A16, Th27, Th35; A22: y in XM by A2, A16, Th26, Th27; consider X being Subset of AS such that A23: p = LDir X and A24: X is being_line by A14, Th20; consider XQ being Subset of AS such that A25: ( ( Q = [XQ,1] & XQ is being_line ) or ( Q = [(PDir XQ),2] & XQ is being_plane ) ) by Th23; A26: x in XP by A7, A20, Th26, Th27; then consider Y being Subset of AS such that A27: XM c= Y and A28: XP c= Y and A29: Y is being_plane by A1, A7, A16, A20, A17, Th27, AFF_4:38; A30: y = b ; A31: X '||' XM by A1, A5, A23, A24, A16, A21, Th27, Th28; then A32: X // XM by A1, A24, A16, A21, Th27, AFF_4:40; A33: y in XQ by A9, A25, Th26, Th27; A34: not XM // XP by A1, A5, A7, A11, A16, A20, A17, A26, Th27, AFF_1:45; A35: now__::_thesis:_(_N_=_[XN,1]_&_XN_is_being_line_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_ (_q_on_P_&_q_on_Q_)_) A36: X // XM by A1, A24, A16, A21, A31, Th27, AFF_4:40; assume that A37: N = [XN,1] and A38: XN is being_line ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) X '||' XN by A6, A23, A24, A37, A38, Th28; then X // XN by A24, A38, AFF_4:40; then A39: XM // XN by A36, AFF_1:44; c is Element of AS proof assume c is not Element of AS ; ::_thesis: contradiction then c = LDir XN by A3, A37, A38, Th34; then XN '||' XP by A7, A8, A20, A21, A38, Th27, Th28; then XN // XP by A7, A20, A21, A38, Th27, AFF_4:40; hence contradiction by A34, A39, AFF_1:44; ::_thesis: verum end; then reconsider z = c as Element of AS ; z in XN by A3, A37, Th26; then A40: XN = z * XM by A1, A16, A21, A39, Th27, AFF_4:def_3; A41: not XN // XQ proof assume XN // XQ ; ::_thesis: contradiction then XM // XQ by A39, AFF_1:44; hence contradiction by A2, A5, A9, A12, A16, A25, A33, A22, Th27, AFF_1:45; ::_thesis: verum end; now__::_thesis:_d_is_Element_of_AS assume d is not Element of AS ; ::_thesis: contradiction then consider Xd being Subset of AS such that A42: d = LDir Xd and A43: Xd is being_line by Th20; Xd '||' XN by A4, A37, A38, A42, A43, Th28; then A44: Xd // XN by A38, A43, AFF_4:40; Xd '||' XQ by A9, A10, A25, A30, A42, A43, Th27, Th28; then Xd // XQ by A9, A25, A30, A43, Th27, AFF_4:40; hence contradiction by A41, A44, AFF_1:44; ::_thesis: verum end; then reconsider w = d as Element of AS ; w in XQ by A10, A25, Th26, Th27; then A45: XQ = Line (y,w) by A9, A18, A25, A33, Th27, AFF_1:57; z in XP by A8, A20, Th26, Th27; then A46: XN c= Y by A1, A16, A21, A27, A28, A29, A40, Th27, AFF_4:28; w in XN by A4, A37, Th26; then XQ c= Y by A18, A27, A29, A22, A46, A45, AFF_4:19; hence ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) by A7, A9, A20, A25, A21, A28, A29, A30, Th27, Th43; ::_thesis: verum end; A47: XP '||' Y by A7, A20, A21, A28, A29, Th27, AFF_4:42; A48: XM '||' Y by A1, A16, A21, A27, A29, Th27, AFF_4:42; now__::_thesis:_(_N_=_[(PDir_XN),2]_&_XN_is_being_plane_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_ (_q_on_P_&_q_on_Q_)_) assume that A49: N = [(PDir XN),2] and A50: XN is being_plane ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) c is not Element of AS by A3, A49, Th27; then c = LDir XP by A7, A8, A20, A21, Th27, Th34; then A51: XP '||' XN by A3, A7, A20, A21, A49, A50, Th27, Th29; d is not Element of AS by A4, A49, Th27; then d = LDir XQ by A9, A10, A25, A30, Th27, Th34; then A52: XQ '||' XN by A4, A9, A25, A30, A49, A50, Th27, Th29; X '||' XN by A6, A23, A24, A49, A50, Th29; then XM '||' XN by A32, AFF_4:56; then XN '||' Y by A1, A5, A7, A11, A16, A20, A17, A26, A29, A48, A47, A50, A51, Th5, Th27, AFF_1:45; then XQ '||' Y by A50, A52, AFF_4:59, AFF_4:60; then XQ c= Y by A9, A25, A27, A29, A33, A22, Th27, AFF_4:43; hence ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) by A7, A9, A20, A25, A21, A28, A29, A30, Th27, Th43; ::_thesis: verum end; hence ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) by A19, A35; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let a, b, c, d, p be POINT of (IncProjSp_of AS); ::_thesis: 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 ) let M, N, P, Q be LINE of (IncProjSp_of AS); ::_thesis: ( 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 ) implies ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) ) assume that A1: a on M and A2: b on M and A3: c on N and A4: d on N and A5: p on M and A6: p on N and A7: a on P and A8: c on P and A9: b on Q and A10: d on Q and A11: not p on P and A12: not p on Q and A13: M <> N and A14: p is not Element of AS and A15: ( a is Element of AS or b is Element of AS or c is Element of AS or d is Element of AS ) ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) now__::_thesis:_(_(_b_is_Element_of_AS_or_d_is_Element_of_AS_)_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_ (_q_on_P_&_q_on_Q_)_) assume ( b is Element of AS or d is Element of AS ) ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) then ex q being POINT of (IncProjSp_of AS) st ( q on Q & q on P ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, Lm10; hence ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) ; ::_thesis: verum end; hence ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, Lm10; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let a, b, c, d, p be POINT of (IncProjSp_of AS); ::_thesis: 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 ) let M, N, P, Q be LINE of (IncProjSp_of AS); ::_thesis: ( 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 implies ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) ) assume that A1: a on M and A2: b on M and A3: c on N and A4: d on N and A5: p on M and A6: p on N and A7: a on P and A8: c on P and A9: b on Q and A10: d on Q and A11: not p on P and A12: not p on Q and A13: M <> N ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) now__::_thesis:_(_p_is_not_Element_of_AS_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_ (_q_on_P_&_q_on_Q_)_) assume A14: p is not Element of AS ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) now__::_thesis:_(_a_is_not_Element_of_AS_&_b_is_not_Element_of_AS_&_c_is_not_Element_of_AS_&_d_is_not_Element_of_AS_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_ (_q_on_P_&_q_on_Q_)_) A15: b <> d by A2, A4, A5, A6, A9, A12, A13, Lm2; set x = the Element of AS; assume that A16: a is not Element of AS and A17: b is not Element of AS and A18: c is not Element of AS and A19: d is not Element of AS ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) consider Xa being Subset of AS such that A20: a = LDir Xa and A21: Xa is being_line by A16, Th20; consider Xc being Subset of AS such that A22: c = LDir Xc and A23: Xc is being_line by A18, Th20; consider Xb being Subset of AS such that A24: b = LDir Xb and A25: Xb is being_line by A17, Th20; consider Xd being Subset of AS such that A26: d = LDir Xd and A27: Xd is being_line by A19, Th20; consider Xp being Subset of AS such that A28: p = LDir Xp and A29: Xp is being_line by A14, Th20; set Xa9 = the Element of AS * Xa; set Xb9 = the Element of AS * Xb; set Xc9 = the Element of AS * Xc; set Xd9 = the Element of AS * Xd; set Xp9 = the Element of AS * Xp; consider y being Element of AS such that A30: the Element of AS <> y and A31: y in the Element of AS * Xa by A21, AFF_1:20, AFF_4:27; A32: Xp // the Element of AS * Xp by A29, AFF_4:def_3; consider t being Element of AS such that A33: the Element of AS <> t and A34: t in the Element of AS * Xc by A23, AFF_1:20, AFF_4:27; set Y1 = y * ( the Element of AS * Xp); set Y2 = t * ( the Element of AS * Xp); A35: the Element of AS * Xp is being_line by A29, AFF_4:27; then A36: y * ( the Element of AS * Xp) is being_line by AFF_4:27; A37: t * ( the Element of AS * Xp) is being_line by A35, AFF_4:27; A38: Xb // the Element of AS * Xb by A25, AFF_4:def_3; A39: the Element of AS * Xd is being_line by A27, AFF_4:27; A40: Xd // the Element of AS * Xd by A27, AFF_4:def_3; A41: the Element of AS in the Element of AS * Xc by A23, AFF_4:def_3; A42: the Element of AS in the Element of AS * Xb by A25, AFF_4:def_3; A43: the Element of AS * Xb is being_line by A25, AFF_4:27; A44: the Element of AS in the Element of AS * Xd by A27, AFF_4:def_3; then consider XQ being Subset of AS such that A45: the Element of AS * Xb c= XQ and A46: the Element of AS * Xd c= XQ and A47: XQ is being_plane by A43, A39, A42, AFF_4:38; A48: the Element of AS * Xa is being_line by A21, AFF_4:27; A49: the Element of AS * Xp // t * ( the Element of AS * Xp) by A35, AFF_4:def_3; A50: not the Element of AS * Xd // t * ( the Element of AS * Xp) proof assume the Element of AS * Xd // t * ( the Element of AS * Xp) ; ::_thesis: contradiction then Xd // t * ( the Element of AS * Xp) by A40, AFF_1:44; then Xd // the Element of AS * Xp by A49, AFF_1:44; then Xd // Xp by A32, AFF_1:44; hence contradiction by A10, A12, A28, A29, A26, A27, Th11; ::_thesis: verum end; A51: the Element of AS * Xp // y * ( the Element of AS * Xp) by A35, AFF_4:def_3; A52: not the Element of AS * Xb // y * ( the Element of AS * Xp) proof assume the Element of AS * Xb // y * ( the Element of AS * Xp) ; ::_thesis: contradiction then Xb // y * ( the Element of AS * Xp) by A38, AFF_1:44; then Xb // the Element of AS * Xp by A51, AFF_1:44; then Xb // Xp by A32, AFF_1:44; hence contradiction by A9, A12, A28, A29, A24, A25, Th11; ::_thesis: verum end; A53: the Element of AS in the Element of AS * Xa by A21, AFF_4:def_3; A54: the Element of AS * Xc is being_line by A23, AFF_4:27; then consider XP being Subset of AS such that A55: the Element of AS * Xa c= XP and A56: the Element of AS * Xc c= XP and A57: XP is being_plane by A48, A53, A41, AFF_4:38; A58: the Element of AS in the Element of AS * Xp by A29, AFF_4:def_3; then consider X2 being Subset of AS such that A59: the Element of AS * Xc c= X2 and A60: the Element of AS * Xp c= X2 and A61: X2 is being_plane by A54, A35, A41, AFF_4:38; A62: Xc // the Element of AS * Xc by A23, AFF_4:def_3; N = [(PDir X2),2] proof reconsider N9 = [(PDir X2),2] as Element of the Lines of (IncProjSp_of AS) by A61, Th23; A63: c on N9 by A22, A62, A59, A61, Th32; p on N9 by A28, A32, A60, A61, Th32; hence N = [(PDir X2),2] by A3, A6, A8, A11, A63, Lm2; ::_thesis: verum end; then Xd '||' X2 by A4, A26, A27, A61, Th29; then A64: the Element of AS * Xd c= X2 by A39, A41, A44, A40, A59, A61, AFF_4:43, AFF_4:56; consider X1 being Subset of the carrier of AS such that A65: the Element of AS * Xa c= X1 and A66: the Element of AS * Xp c= X1 and A67: X1 is being_plane by A48, A35, A53, A58, AFF_4:38; A68: Xa // the Element of AS * Xa by A21, AFF_4:def_3; M = [(PDir X1),2] proof reconsider M9 = [(PDir X1),2] as Element of the Lines of (IncProjSp_of AS) by A67, Th23; A69: a on M9 by A20, A68, A65, A67, Th32; p on M9 by A28, A32, A66, A67, Th32; hence M = [(PDir X1),2] by A1, A5, A7, A11, A69, Lm2; ::_thesis: verum end; then Xb '||' X1 by A2, A24, A25, A67, Th29; then A70: the Element of AS * Xb c= X1 by A43, A53, A42, A38, A65, A67, AFF_4:43, AFF_4:56; y * ( the Element of AS * Xp) c= X1 by A29, A31, A65, A66, A67, AFF_4:27, AFF_4:28; then consider z being Element of AS such that A71: z in the Element of AS * Xb and A72: z in y * ( the Element of AS * Xp) by A43, A36, A67, A70, A52, AFF_4:22; t * ( the Element of AS * Xp) c= X2 by A29, A34, A59, A60, A61, AFF_4:27, AFF_4:28; then consider u being Element of AS such that A73: u in the Element of AS * Xd and A74: u in t * ( the Element of AS * Xp) by A39, A37, A61, A64, A50, AFF_4:22; set AC = Line (y,t); set BD = Line (z,u); A75: y in Line (y,t) by AFF_1:15; A76: y in y * ( the Element of AS * Xp) by A35, AFF_4:def_3; A77: the Element of AS <> z proof assume A78: not the Element of AS <> z ; ::_thesis: contradiction a = LDir ( the Element of AS * Xa) by A20, A21, A48, A68, Th11 .= LDir (y * ( the Element of AS * Xp)) by A48, A53, A30, A31, A36, A76, A72, A78, AFF_1:18 .= LDir ( the Element of AS * Xp) by A35, A36, A51, Th11 .= p by A28, A29, A35, A32, Th11 ; hence contradiction by A7, A11; ::_thesis: verum end; A79: z <> u proof assume A80: not z <> u ; ::_thesis: contradiction b = LDir ( the Element of AS * Xb) by A24, A25, A43, A38, Th11 .= LDir ( the Element of AS * Xd) by A43, A39, A42, A44, A71, A73, A77, A80, AFF_1:18 .= d by A26, A27, A39, A40, Th11 ; hence contradiction by A2, A4, A5, A6, A9, A12, A13, Lm2; ::_thesis: verum end; then A81: Line (z,u) is being_line by AFF_1:def_3; A82: the Element of AS * Xa <> the Element of AS * Xc proof assume the Element of AS * Xa = the Element of AS * Xc ; ::_thesis: contradiction then a = LDir ( the Element of AS * Xc) by A20, A21, A48, A68, Th11 .= c by A22, A23, A54, A62, Th11 ; hence contradiction by A1, A3, A5, A6, A7, A11, A13, Lm2; ::_thesis: verum end; then A83: y <> t by A48, A54, A53, A41, A30, A31, A34, AFF_1:18; then A84: Line (y,t) is being_line by AFF_1:def_3; A85: Line (z,u) c= XQ by A71, A73, A79, A45, A46, A47, AFF_4:19; A86: t in Line (y,t) by AFF_1:15; y * ( the Element of AS * Xp) // t * ( the Element of AS * Xp) by A51, A49, AFF_1:44; then consider X3 being Subset of AS such that A87: y * ( the Element of AS * Xp) c= X3 and A88: t * ( the Element of AS * Xp) c= X3 and A89: X3 is being_plane by AFF_4:39; A90: Line (z,u) c= X3 by A87, A88, A89, A72, A74, A79, AFF_4:19; A91: a <> c by A1, A3, A5, A6, A7, A11, A13, Lm2; A92: ( P = [(PDir XP),2] & Q = [(PDir XQ),2] ) proof reconsider P9 = [(PDir XP),2], Q9 = [(PDir XQ),2] as LINE of (IncProjSp_of AS) by A57, A47, Th23; A93: c on P9 by A22, A62, A56, A57, Th32; A94: b on Q9 by A24, A38, A45, A47, Th32; A95: d on Q9 by A26, A40, A46, A47, Th32; a on P9 by A20, A68, A55, A57, Th32; hence ( P = [(PDir XP),2] & Q = [(PDir XQ),2] ) by A7, A8, A9, A10, A91, A15, A93, A94, A95, Lm2; ::_thesis: verum end; A96: now__::_thesis:_(_Line_(y,t)_//_Line_(z,u)_implies_ex_q_being_Element_of_the_Points_of_(IncProjSp_of_AS)_st_ (_q_on_P_&_q_on_Q_)_) reconsider q = LDir (Line (y,t)), q9 = LDir (Line (z,u)) as Element of the Points of (IncProjSp_of AS) by A84, A81, Th20; assume A97: Line (y,t) // Line (z,u) ; ::_thesis: ex q being Element of the Points of (IncProjSp_of AS) st ( q on P & q on Q ) take q = q; ::_thesis: ( q on P & q on Q ) q = q9 by A84, A81, A97, Th11; hence ( q on P & q on Q ) by A31, A34, A71, A73, A83, A79, A84, A81, A55, A56, A57, A45, A46, A47, A92, Th31, AFF_4:19; ::_thesis: verum end; A98: Line (y,t) c= XP by A31, A34, A83, A55, A56, A57, AFF_4:19; A99: now__::_thesis:_(_ex_w_being_Element_of_AS_st_ (_w_in_Line_(y,t)_&_w_in_Line_(z,u)_)_implies_ex_q_being_POINT_of_(IncProjSp_of_AS)_st_ (_q_on_P_&_q_on_Q_)_) given w being Element of AS such that A100: w in Line (y,t) and A101: w in Line (z,u) ; ::_thesis: ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) set R = Line ( the Element of AS,w); A102: the Element of AS <> w proof assume A103: the Element of AS = w ; ::_thesis: contradiction then the Element of AS * Xa = Line (y,t) by A48, A53, A30, A31, A84, A75, A100, AFF_1:18; hence contradiction by A54, A41, A33, A34, A82, A84, A86, A100, A103, AFF_1:18; ::_thesis: verum end; then A104: Line ( the Element of AS,w) is being_line by AFF_1:def_3; then reconsider q = LDir (Line ( the Element of AS,w)) as POINT of (IncProjSp_of AS) by Th20; take q = q; ::_thesis: ( q on P & q on Q ) thus ( q on P & q on Q ) by A53, A42, A55, A57, A45, A47, A92, A98, A85, A100, A101, A102, A104, Th31, AFF_4:19; ::_thesis: verum end; t in t * ( the Element of AS * Xp) by A35, AFF_4:def_3; then Line (y,t) c= X3 by A76, A87, A88, A89, A83, AFF_4:19; hence ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) by A89, A84, A81, A90, A96, A99, AFF_4:22; ::_thesis: verum end; hence ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, Lm11; ::_thesis: verum end; hence ex q being POINT of (IncProjSp_of AS) st ( q on P & q on Q ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, Lm9; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let a, b, c, d, p be Element of the Points of (ProjHorizon AS); ::_thesis: 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 ) let M, N, P, Q be Element of the Lines of (ProjHorizon AS); ::_thesis: ( 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 implies ex q being Element of the Points of (ProjHorizon AS) st ( q on P & q on Q ) ) assume that A1: a on M and A2: b on M and A3: c on N and A4: d on N and A5: p on M and A6: p on N and A7: a on P and A8: c on P and A9: b on Q and A10: d on Q and A11: not p on P and A12: not p on Q and A13: M <> N ; ::_thesis: ex q being Element of the Points of (ProjHorizon AS) st ( q on P & q on Q ) reconsider M9 = [M,2], N9 = [N,2], P9 = [P,2], Q9 = [Q,2] as LINE of (IncProjSp_of AS) by Th25; reconsider a9 = a, b9 = b, c9 = c, d9 = d, p9 = p as POINT of (IncProjSp_of AS) by Th22; A14: b9 on M9 by A2, Th37; A15: M9 <> N9 proof assume M9 = N9 ; ::_thesis: contradiction then M = [N,2] `1 by MCART_1:7 .= N ; hence contradiction by A13; ::_thesis: verum end; A16: d9 on N9 by A4, Th37; A17: c9 on N9 by A3, Th37; A18: c9 on P9 by A8, Th37; A19: a9 on P9 by A7, Th37; A20: p9 on N9 by A6, Th37; A21: p9 on M9 by A5, Th37; A22: not p9 on Q9 by A12, Th37; A23: not p9 on P9 by A11, Th37; A24: d9 on Q9 by A10, Th37; A25: b9 on Q9 by A9, Th37; a9 on M9 by A1, Th37; then consider q9 being POINT of (IncProjSp_of AS) such that A26: q9 on P9 and A27: q9 on Q9 by A14, A17, A16, A21, A20, A19, A18, A25, A24, A23, A22, A15, Lm12; [q9,[P,2]] in the Inc of (IncProjSp_of AS) by A26, INCSP_1:def_1; then reconsider q = q9 as Element of the Points of (ProjHorizon AS) by Th42; take q ; ::_thesis: ( q on P & q on Q ) thus ( q on P & q on Q ) by A26, A27, Th37; ::_thesis: verum end; 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 ); proof set XX = IncProjSp_of AS; A1: for a, b being POINT of (IncProjSp_of AS) ex A being LINE of (IncProjSp_of AS) st ( a on A & b on A ) by Lm4; A2: not for a being POINT of (IncProjSp_of AS) for A being LINE of (IncProjSp_of AS) holds a on A by Lm6; A3: for A being LINE of (IncProjSp_of AS) ex a, b, c being POINT of (IncProjSp_of AS) st ( a <> b & b <> c & c <> a & a on A & b on A & c on A ) proof let A be LINE of (IncProjSp_of AS); ::_thesis: ex a, b, c being POINT of (IncProjSp_of AS) st ( a <> b & b <> c & c <> a & a on A & b on A & c on A ) consider a, b, c being POINT of (IncProjSp_of AS) such that A4: a on A and A5: b on A and A6: c on A and A7: a <> b and A8: b <> c and A9: c <> a by Lm3; take a ; ::_thesis: ex b, c being POINT of (IncProjSp_of AS) st ( a <> b & b <> c & c <> a & a on A & b on A & c on A ) take b ; ::_thesis: ex c being POINT of (IncProjSp_of AS) st ( a <> b & b <> c & c <> a & a on A & b on A & c on A ) take c ; ::_thesis: ( a <> b & b <> c & c <> a & a on A & b on A & c on A ) thus ( a <> b & b <> c & c <> a & a on A & b on A & c on A ) by A4, A5, A6, A7, A8, A9; ::_thesis: verum end; A10: for a, b, c, d, p, q 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 ) by Lm12; for a, b being POINT of (IncProjSp_of AS) for A, K being LINE of (IncProjSp_of AS) st a on A & b on A & a on K & b on K & not a = b holds A = K by Lm2; hence ( 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 ) by A1, A2, A3, A10, INCPROJ:def_4, INCPROJ:def_5, INCPROJ:def_6, INCPROJ:def_7, INCPROJ:def_8; ::_thesis: verum end; 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 ) proof set AS = the AffinPlane; set XX = IncProjSp_of the AffinPlane; for A, K being LINE of (IncProjSp_of the AffinPlane) ex a being POINT of (IncProjSp_of the AffinPlane) st ( a on A & a on K ) by Lm5; then IncProjSp_of the AffinPlane is 2-dimensional IncProjSp by INCPROJ:def_9; hence ex b1 being IncProjSp st ( b1 is strict & b1 is 2-dimensional ) ; ::_thesis: verum end; end; registration let AS be AffinPlane; cluster IncProjSp_of AS -> strict 2-dimensional ; correctness coherence IncProjSp_of AS is 2-dimensional ; proof set XX = IncProjSp_of AS; for A, K being LINE of (IncProjSp_of AS) ex a being Element of the Points of (IncProjSp_of AS) st ( a on A & a on K ) by Lm5; hence IncProjSp_of AS is 2-dimensional by INCPROJ:def_9; ::_thesis: verum end; end; theorem :: AFPROJ:45 for AS being AffinSpace st IncProjSp_of AS is 2-dimensional holds AS is AffinPlane proof let AS be AffinSpace; ::_thesis: ( IncProjSp_of AS is 2-dimensional implies AS is AffinPlane ) set x = the Element of AS; assume A1: IncProjSp_of AS is 2-dimensional ; ::_thesis: AS is AffinPlane consider X being Subset of AS such that A2: the Element of AS in X and the Element of AS in X and the Element of AS in X and A3: X is being_plane by AFF_4:37; assume AS is not AffinPlane ; ::_thesis: contradiction then consider z being Element of AS such that A4: not z in X by A3, AFF_4:48; set Y = Line ( the Element of AS,z); A5: Line ( the Element of AS,z) is being_line by A2, A4, AFF_1:def_3; then reconsider A = [(PDir X),2], K = [(Line ( the Element of AS,z)),1] as LINE of (IncProjSp_of AS) by A3, Th23; consider a being POINT of (IncProjSp_of AS) such that A6: a on A and A7: a on K by A1, INCPROJ:def_9; a is not Element of AS by A6, Th27; then consider Y9 being Subset of AS such that A8: a = LDir Y9 and A9: Y9 is being_line by Th20; Y9 '||' Line ( the Element of AS,z) by A5, A7, A8, A9, Th28; then A10: Y9 // Line ( the Element of AS,z) by A5, A9, AFF_4:40; A11: z in Line ( the Element of AS,z) by AFF_1:15; A12: the Element of AS in Line ( the Element of AS,z) by AFF_1:15; Y9 '||' X by A3, A6, A8, A9, Th29; then Line ( the Element of AS,z) c= X by A2, A3, A5, A12, A10, AFF_4:43, AFF_4:56; hence contradiction by A4, A11; ::_thesis: verum end; theorem :: AFPROJ:46 for AS being AffinSpace st AS is not AffinPlane holds ProjHorizon AS is IncProjSp proof let AS be AffinSpace; ::_thesis: ( AS is not AffinPlane implies ProjHorizon AS is IncProjSp ) set XX = ProjHorizon AS; A1: 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 ) by Th40; A2: for A being Element of the Lines of (ProjHorizon AS) ex a, b, c being Element of the Points of (ProjHorizon AS) st ( a <> b & b <> c & c <> a & a on A & b on A & c on A ) proof let A be Element of the Lines of (ProjHorizon AS); ::_thesis: ex a, b, c being Element of the Points of (ProjHorizon AS) st ( a <> b & b <> c & c <> a & a on A & b on A & c on A ) consider a, b, c being Element of the Points of (ProjHorizon AS) such that A3: a on A and A4: b on A and A5: c on A and A6: a <> b and A7: b <> c and A8: c <> a by Th39; take a ; ::_thesis: ex b, c being Element of the Points of (ProjHorizon AS) st ( a <> b & b <> c & c <> a & a on A & b on A & c on A ) take b ; ::_thesis: ex c being Element of the Points of (ProjHorizon AS) st ( a <> b & b <> c & c <> a & a on A & b on A & c on A ) take c ; ::_thesis: ( a <> b & b <> c & c <> a & a on A & b on A & c on A ) thus ( a <> b & b <> c & c <> a & a on A & b on A & c on A ) by A3, A4, A5, A6, A7, A8; ::_thesis: verum end; assume AS is not AffinPlane ; ::_thesis: ProjHorizon AS is IncProjSp then A9: not for a being Element of the Points of (ProjHorizon AS) for A being Element of the Lines of (ProjHorizon AS) holds a on A by Lm1; A10: for a, b, c, d, p, q 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 ) by Th44; 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 & b on A & a on K & b on K & not a = b holds A = K by Th38; hence ProjHorizon AS is IncProjSp by A1, A9, A2, A10, INCPROJ:def_4, INCPROJ:def_5, INCPROJ:def_6, INCPROJ:def_7, INCPROJ:def_8; ::_thesis: verum end; theorem :: AFPROJ:47 for AS being AffinSpace st ProjHorizon AS is IncProjSp holds not AS is AffinPlane proof let AS be AffinSpace; ::_thesis: ( ProjHorizon AS is IncProjSp implies not AS is AffinPlane ) set XX = ProjHorizon AS; assume ProjHorizon AS is IncProjSp ; ::_thesis: AS is not AffinPlane then consider a being Element of the Points of (ProjHorizon AS), A being Element of the Lines of (ProjHorizon AS) such that A1: not a on A by INCPROJ:def_6; consider X being Subset of AS such that A2: a = LDir X and A3: X is being_line by Th14; consider Y being Subset of AS such that A4: A = PDir Y and A5: Y is being_plane by Th15; assume AS is AffinPlane ; ::_thesis: contradiction then Y = the carrier of AS by A5, Th2; then X '||' Y by A3, A5, AFF_4:42; hence contradiction by A1, A2, A3, A4, A5, Th36; ::_thesis: verum end; 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 proof let AS be AffinSpace; ::_thesis: 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 let M, N be Subset of AS; ::_thesis: 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 let o, a, b, c, a9, b9, c9 be Element of AS; ::_thesis: ( 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 ) implies a,c9 // c,a9 ) assume that A1: M is being_line and A2: N is being_line and A3: M <> N and A4: o in M and A5: o in N and A6: o <> b and A7: o <> b9 and A8: o <> c9 and A9: b in M and A10: c in M and A11: a9 in N and A12: b9 in N and A13: c9 in N and A14: a,b9 // b,a9 and A15: b,c9 // c,b9 and A16: ( a = b or b = c or a = c ) ; ::_thesis: a,c9 // c,a9 A17: c <> b9 by A1, A2, A3, A4, A5, A7, A10, A12, AFF_1:18; now__::_thesis:_(_a_=_c_implies_a,c9_//_c,a9_) assume A18: a = c ; ::_thesis: a,c9 // c,a9 then b,c9 // b,a9 by A14, A15, A17, AFF_1:5; then a9 = c9 by A1, A2, A3, A4, A5, A6, A8, A9, A11, A13, AFF_4:9; hence a,c9 // c,a9 by A18, AFF_1:2; ::_thesis: verum end; hence a,c9 // c,a9 by A1, A2, A3, A4, A5, A6, A7, A8, A9, A11, A12, A13, A14, A15, A16, AFF_4:9; ::_thesis: verum end; theorem :: AFPROJ:49 for AS being AffinSpace st IncProjSp_of AS is Pappian holds AS is Pappian proof let AS be AffinSpace; ::_thesis: ( IncProjSp_of AS is Pappian implies AS is Pappian ) set XX = IncProjSp_of AS; assume A1: IncProjSp_of AS is Pappian ; ::_thesis: AS is Pappian 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 <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds a,c9 // c,a9 proof let M, N be Subset of AS; ::_thesis: 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 <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds a,c9 // c,a9 let o, a, b, c, a9, b9, c9 be Element of AS; ::_thesis: ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 ) assume that A2: M is being_line and A3: N is being_line and A4: M <> N and A5: o in M and A6: o in N and A7: o <> a and A8: o <> a9 and A9: o <> b and A10: o <> b9 and A11: o <> c and A12: o <> c9 and A13: a in M and A14: b in M and A15: c in M and A16: a9 in N and A17: b9 in N and A18: c9 in N and A19: a,b9 // b,a9 and A20: b,c9 // c,b9 ; ::_thesis: a,c9 // c,a9 A21: b <> c9 by A2, A3, A4, A5, A6, A9, A14, A18, AFF_1:18; then A22: Line (b,c9) is being_line by AFF_1:def_3; c <> a9 by A2, A3, A4, A5, A6, A8, A15, A16, AFF_1:18; then A23: Line (c,a9) is being_line by AFF_1:def_3; A24: b <> a9 by A2, A3, A4, A5, A6, A8, A14, A16, AFF_1:18; then A25: Line (b,a9) is being_line by AFF_1:def_3; A26: c <> b9 by A2, A3, A4, A5, A6, A10, A15, A17, AFF_1:18; then A27: Line (c,b9) is being_line by AFF_1:def_3; reconsider A3 = [M,1], B3 = [N,1] as Element of the Lines of (IncProjSp_of AS) by A2, A3, Th23; reconsider p = o, a1 = a9, a2 = c9, a3 = b9, b1 = a, b2 = c, b3 = b as Element of the Points of (IncProjSp_of AS) by Th20; A28: p on A3 by A2, A5, Th26; A29: a <> b9 by A2, A3, A4, A5, A6, A7, A13, A17, AFF_1:18; then A30: Line (a,b9) is being_line by AFF_1:def_3; then reconsider c1 = LDir (Line (b,c9)), c2 = LDir (Line (a,b9)) as Element of the Points of (IncProjSp_of AS) by A22, Th20; A31: b1 on A3 by A2, A13, Th26; a <> c9 by A2, A3, A4, A5, A6, A7, A13, A18, AFF_1:18; then A32: Line (a,c9) is being_line by AFF_1:def_3; then reconsider A1 = [(Line (b,c9)),1], A2 = [(Line (b,a9)),1], B1 = [(Line (a,b9)),1], B2 = [(Line (c,b9)),1], C1 = [(Line (c,a9)),1], C2 = [(Line (a,c9)),1] as Element of the Lines of (IncProjSp_of AS) by A30, A25, A22, A27, A23, Th23; A33: c2 on B1 by A30, Th30; A34: b3 on A3 by A2, A14, Th26; A35: b2 on A3 by A2, A15, Th26; consider Y being Subset of AS such that A36: M c= Y and A37: N c= Y and A38: Y is being_plane by A2, A3, A5, A6, AFF_4:38; reconsider C39 = [(PDir Y),2] as Element of the Lines of (IncProjSp_of AS) by A38, Th23; A39: c1 on C39 by A14, A18, A36, A37, A38, A21, A22, Th31, AFF_4:19; A40: c2 on C39 by A13, A17, A36, A37, A38, A29, A30, Th31, AFF_4:19; A41: a1 on B3 by A3, A16, Th26; A42: a3 on B3 by A3, A17, Th26; A43: p on B3 by A3, A6, Th26; b9 in Line (a,b9) by AFF_1:15; then A44: a3 on B1 by A30, Th26; a in Line (a,b9) by AFF_1:15; then A45: b1 on B1 by A30, Th26; A46: c in Line (c,a9) by AFF_1:15; then A47: b2 on C1 by A23, Th26; Line (b,c9) // Line (c,b9) by A20, A21, A26, AFF_1:37; then Line (b,c9) '||' Line (c,b9) by A22, A27, AFF_4:40; then A48: c1 on B2 by A22, A27, Th28; A49: c9 in Line (a,c9) by AFF_1:15; then A50: a2 on C2 by A32, Th26; b9 in Line (c,b9) by AFF_1:15; then A51: a3 on B2 by A27, Th26; c in Line (c,b9) by AFF_1:15; then A52: b2 on B2 by A27, Th26; c9 in Line (b,c9) by AFF_1:15; then A53: a2 on A1 by A22, Th26; b in Line (b,c9) by AFF_1:15; then A54: b3 on A1 by A22, Th26; A55: a2 on B3 by A3, A18, Th26; Line (a,b9) // Line (b,a9) by A19, A29, A24, AFF_1:37; then Line (a,b9) '||' Line (b,a9) by A30, A25, AFF_4:40; then A56: c2 on A2 by A30, A25, Th28; A57: a in Line (a,c9) by AFF_1:15; then A58: b1 on C2 by A32, Th26; a9 in Line (b,a9) by AFF_1:15; then A59: a1 on A2 by A25, Th26; b in Line (b,a9) by AFF_1:15; then A60: b3 on A2 by A25, Th26; A61: a9 in Line (c,a9) by AFF_1:15; then A62: a1 on C1 by A23, Th26; A63: c1 on A1 by A22, Th30; now__::_thesis:_(_b1_<>_b2_&_b2_<>_b3_&_b3_<>_b1_implies_a,c9_//_c,a9_) A64: A3 <> B3 proof assume A3 = B3 ; ::_thesis: contradiction then M = [N,1] `1 by MCART_1:7 .= N ; hence contradiction by A4; ::_thesis: verum end; ( not p on C1 & not p on C2 ) proof assume ( p on C1 or p on C2 ) ; ::_thesis: contradiction then ( a1 on A3 or a2 on A3 ) by A7, A11, A28, A31, A35, A58, A50, A47, A62, Lm2; hence contradiction by A8, A12, A28, A43, A41, A55, A64, INCPROJ:def_4; ::_thesis: verum end; then consider c3 being Element of the Points of (IncProjSp_of AS) such that A65: c3 on C1 and A66: c3 on C2 by A28, A31, A35, A43, A41, A55, A58, A50, A47, A62, A64, INCPROJ:def_8; A67: {a2,b1,c3} on C2 by A58, A50, A66, INCSP_1:2; A68: {a1,b3,c2} on A2 by A60, A59, A56, INCSP_1:2; A69: {a3,b1,c2} on B1 by A45, A44, A33, INCSP_1:2; assume that A70: b1 <> b2 and A71: b2 <> b3 and A72: b3 <> b1 ; ::_thesis: a,c9 // c,a9 A73: p,b1,b2,b3 are_mutually_different by A7, A9, A11, A70, A71, A72, ZFMISC_1:def_6; ( a1 <> a2 & a2 <> a3 & a1 <> a3 ) proof A74: now__::_thesis:_not_a9_=_c9 assume a9 = c9 ; ::_thesis: contradiction then a,b9 // c,b9 by A19, A20, A24, AFF_1:5; hence contradiction by A2, A3, A4, A5, A6, A7, A10, A13, A15, A17, A70, AFF_4:9; ::_thesis: verum end; assume ( not a1 <> a2 or not a2 <> a3 or not a1 <> a3 ) ; ::_thesis: contradiction hence contradiction by A2, A3, A4, A5, A6, A7, A9, A10, A13, A14, A15, A17, A19, A20, A71, A72, A74, AFF_4:9; ::_thesis: verum end; then A75: p,a1,a2,a3 are_mutually_different by A8, A10, A12, ZFMISC_1:def_6; A76: {a1,a2,a3} on B3 by A41, A55, A42, INCSP_1:2; A77: {b1,b2,b3} on A3 by A31, A35, A34, INCSP_1:2; A78: {a3,b2,c1} on B2 by A51, A52, A48, INCSP_1:2; A79: {a2,b3,c1} on A1 by A53, A54, A63, INCSP_1:2; A80: p on B3 by A3, A6, Th26; A81: p on A3 by A2, A5, Th26; A82: {c1,c2} on C39 by A39, A40, INCSP_1:1; {a1,b2,c3} on C1 by A47, A62, A65, INCSP_1:2; then c3 on C39 by A1, A75, A73, A64, A81, A80, A79, A69, A68, A78, A67, A77, A76, A82, INCPROJ:def_14; then c3 is not Element of AS by Th27; then consider Y being Subset of AS such that A83: c3 = LDir Y and A84: Y is being_line by Th20; Y '||' Line (c,a9) by A23, A65, A83, A84, Th28; then A85: Y // Line (c,a9) by A23, A84, AFF_4:40; Y '||' Line (a,c9) by A32, A66, A83, A84, Th28; then Y // Line (a,c9) by A32, A84, AFF_4:40; then Line (a,c9) // Line (c,a9) by A85, AFF_1:44; hence a,c9 // c,a9 by A57, A49, A46, A61, AFF_1:39; ::_thesis: verum end; hence a,c9 // c,a9 by A2, A3, A4, A5, A6, A9, A10, A12, A14, A15, A16, A17, A18, A19, A20, Th48; ::_thesis: verum end; hence AS is Pappian by AFF_2:def_2; ::_thesis: verum end; 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 proof let AS be AffinSpace; ::_thesis: 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 let A, P, C be Subset of AS; ::_thesis: 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 let o, a, b, c, a9, b9, c9 be Element of AS; ::_thesis: ( 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 ) implies b,c // b9,c9 ) assume that A1: o in A and A2: o in P and A3: o in C and A4: o <> a and A5: o <> b and A6: o <> c and A7: a in A and A8: b in P and A9: b9 in P and A10: c in C and A11: c9 in C and A12: A is being_line and A13: P is being_line and A14: C is being_line and A15: A <> P and A16: A <> C and A17: a,b // a9,b9 and A18: a,c // a9,c9 and A19: ( o = a9 or a = a9 ) ; ::_thesis: b,c // b9,c9 A20: now__::_thesis:_(_a_=_a9_implies_b,c_//_b9,c9_) assume A21: a = a9 ; ::_thesis: b,c // b9,c9 then A22: c = c9 by A1, A3, A4, A6, A7, A10, A11, A12, A14, A16, A18, AFF_4:9; b = b9 by A1, A2, A4, A5, A7, A8, A9, A12, A13, A15, A17, A21, AFF_4:9; hence b,c // b9,c9 by A22, AFF_1:2; ::_thesis: verum end; now__::_thesis:_(_o_=_a9_implies_b,c_//_b9,c9_) assume A23: o = a9 ; ::_thesis: b,c // b9,c9 then A24: o = c9 by A1, A3, A4, A6, A7, A10, A11, A12, A14, A16, A18, AFF_4:8; o = b9 by A1, A2, A4, A5, A7, A8, A9, A12, A13, A15, A17, A23, AFF_4:8; hence b,c // b9,c9 by A24, AFF_1:3; ::_thesis: verum end; hence b,c // b9,c9 by A19, A20; ::_thesis: verum end; theorem :: AFPROJ:51 for AS being AffinSpace st IncProjSp_of AS is Desarguesian holds AS is Desarguesian proof let AS be AffinSpace; ::_thesis: ( IncProjSp_of AS is Desarguesian implies AS is Desarguesian ) set XX = IncProjSp_of AS; assume A1: IncProjSp_of AS is Desarguesian ; ::_thesis: AS is Desarguesian 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 & a9 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 holds b,c // b9,c9 proof let A, P, C be Subset of AS; ::_thesis: 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 & a9 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 holds b,c // b9,c9 let o, a, b, c, a9, b9, c9 be Element of AS; ::_thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 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 implies b,c // b9,c9 ) assume that A2: o in A and A3: o in P and A4: o in C and A5: o <> a and A6: o <> b and A7: o <> c and A8: a in A and A9: a9 in A and A10: b in P and A11: b9 in P and A12: c in C and A13: c9 in C and A14: A is being_line and A15: P is being_line and A16: C is being_line and A17: A <> P and A18: A <> C and A19: a,b // a9,b9 and A20: a,c // a9,c9 ; ::_thesis: b,c // b9,c9 now__::_thesis:_(_P_<>_C_implies_b,c_//_b9,c9_) assume A21: P <> C ; ::_thesis: b,c // b9,c9 now__::_thesis:_(_a_<>_a9_&_o_<>_a9_implies_b,c_//_b9,c9_) reconsider p = o, a1 = a, b1 = a9, a2 = b, b2 = b9, a3 = c, b3 = c9 as Element of the Points of (IncProjSp_of AS) by Th20; reconsider C1 = [A,1], C2 = [P,1], C39 = [C,1] as Element of the Lines of (IncProjSp_of AS) by A14, A15, A16, Th23; assume that A22: a <> a9 and A23: o <> a9 ; ::_thesis: b,c // b9,c9 A24: o <> c9 by A2, A4, A5, A7, A8, A9, A12, A14, A16, A18, A20, A23, AFF_4:8; A25: a9 <> c9 by A2, A4, A9, A13, A14, A16, A18, A23, AFF_1:18; then A26: Line (a9,c9) is being_line by AFF_1:def_3; A27: o <> b9 by A2, A3, A5, A6, A8, A9, A10, A14, A15, A17, A19, A23, AFF_4:8; then b9 <> c9 by A3, A4, A11, A13, A15, A16, A21, AFF_1:18; then A28: Line (b9,c9) is being_line by AFF_1:def_3; b <> c by A3, A4, A6, A10, A12, A15, A16, A21, AFF_1:18; then A29: Line (b,c) is being_line by AFF_1:def_3; A30: a <> c by A2, A4, A5, A8, A12, A14, A16, A18, AFF_1:18; then A31: Line (a,c) is being_line by AFF_1:def_3; A32: a <> b by A2, A3, A5, A8, A10, A14, A15, A17, AFF_1:18; then A33: Line (a,b) is being_line by AFF_1:def_3; then reconsider s = LDir (Line (a,b)), r = LDir (Line (a,c)) as Element of the Points of (IncProjSp_of AS) by A31, Th20; A34: p on C2 by A3, A15, Th26; A35: a9 <> b9 by A2, A3, A9, A11, A14, A15, A17, A23, AFF_1:18; then A36: Line (a9,b9) is being_line by AFF_1:def_3; then reconsider A1 = [(Line (b,c)),1], A2 = [(Line (a,c)),1], A3 = [(Line (a,b)),1], B1 = [(Line (b9,c9)),1], B2 = [(Line (a9,c9)),1], B3 = [(Line (a9,b9)),1] as Element of the Lines of (IncProjSp_of AS) by A33, A29, A31, A28, A26, Th23; A37: r on A2 by A31, Th30; A38: c in Line (b,c) by AFF_1:15; then A39: a3 on A1 by A29, Th26; A40: a3 on A1 by A29, A38, Th26; A41: c9 in Line (a9,c9) by AFF_1:15; then A42: b3 on B2 by A26, Th26; A43: a9 in Line (a9,c9) by AFF_1:15; then A44: b1 on B2 by A26, Th26; A45: Line (a,c) // Line (a9,c9) by A20, A30, A25, AFF_1:37; then Line (a,c) '||' Line (a9,c9) by A31, A26, AFF_4:40; then r on B2 by A31, A26, Th28; then A46: {b1,r,b3} on B2 by A44, A42, INCSP_1:2; A47: c <> c9 by A2, A4, A5, A7, A8, A9, A12, A14, A16, A18, A20, A22, AFF_4:9; A48: b1 on C1 by A9, A14, Th26; A49: a3 on C39 by A12, A16, Th26; A50: b9 in Line (a9,b9) by AFF_1:15; then A51: b2 on B3 by A36, Th26; A52: a9 in Line (a9,b9) by AFF_1:15; then A53: b1 on B3 by A36, Th26; A54: Line (a,b) // Line (a9,b9) by A19, A32, A35, AFF_1:37; then Line (a,b) '||' Line (a9,b9) by A33, A36, AFF_4:40; then s on B3 by A33, A36, Th28; then A55: {b1,s,b2} on B3 by A53, A51, INCSP_1:2; A56: now__::_thesis:_not_C2_=_C39 assume C2 = C39 ; ::_thesis: contradiction then P = [C,1] `1 by MCART_1:7 .= C ; hence contradiction by A21; ::_thesis: verum end; A57: now__::_thesis:_not_C1_=_C39 assume C1 = C39 ; ::_thesis: contradiction then A = [C,1] `1 by MCART_1:7 .= C ; hence contradiction by A18; ::_thesis: verum end; now__::_thesis:_not_C1_=_C2 assume C1 = C2 ; ::_thesis: contradiction then A = [P,1] `1 by MCART_1:7 .= P ; hence contradiction by A17; ::_thesis: verum end; then A58: C1,C2,C39 are_mutually_different by A56, A57, ZFMISC_1:def_5; A59: a1 on C1 by A8, A14, Th26; A60: b3 on C39 by A13, A16, Th26; A61: p on C39 by A4, A16, Th26; then A62: {p,a3,b3} on C39 by A49, A60, INCSP_1:2; p on C1 by A2, A14, Th26; then A63: {p,b1,a1} on C1 by A48, A59, INCSP_1:2; A64: b2 on C2 by A11, A15, Th26; A65: a in Line (a,c) by AFF_1:15; then A66: a1 on A2 by A31, Th26; A67: c in Line (a,c) by AFF_1:15; then a3 on A2 by A31, Th26; then A68: {a3,r,a1} on A2 by A37, A66, INCSP_1:2; A69: b9 in Line (b9,c9) by AFF_1:15; then A70: b2 on B1 by A28, Th26; A71: c9 in Line (b9,c9) by AFF_1:15; then A72: b3 on B1 by A28, Th26; A73: b3 on B1 by A28, A71, Th26; A74: a2 on C2 by A10, A15, Th26; then A75: {p,a2,b2} on C2 by A34, A64, INCSP_1:2; A76: b in Line (b,c) by AFF_1:15; then A77: a2 on A1 by A29, Th26; ( not p on A1 & not p on B1 ) proof assume ( p on A1 or p on B1 ) ; ::_thesis: contradiction then ( a3 on C2 or b3 on C2 ) by A6, A27, A34, A74, A64, A77, A40, A70, A73, INCPROJ:def_4; hence contradiction by A7, A24, A34, A61, A49, A60, A56, INCPROJ:def_4; ::_thesis: verum end; then consider t being Element of the Points of (IncProjSp_of AS) such that A78: t on A1 and A79: t on B1 by A34, A61, A74, A64, A49, A60, A77, A40, A70, A73, A56, INCPROJ:def_8; a2 on A1 by A29, A76, Th26; then A80: {a3,a2,t} on A1 by A78, A39, INCSP_1:2; b2 on B1 by A28, A69, Th26; then A81: {t,b2,b3} on B1 by A79, A72, INCSP_1:2; A82: a in Line (a,b) by AFF_1:15; then A83: a1 on A3 by A33, Th26; A84: s on A3 by A33, Th30; A85: b in Line (a,b) by AFF_1:15; then a2 on A3 by A33, Th26; then A86: {a2,s,a1} on A3 by A84, A83, INCSP_1:2; b <> b9 by A2, A3, A5, A6, A8, A9, A10, A14, A15, A17, A19, A22, AFF_4:9; then consider O being Element of the Lines of (IncProjSp_of AS) such that A87: {r,s,t} on O by A1, A5, A6, A7, A22, A23, A27, A24, A47, A63, A75, A62, A80, A68, A86, A81, A46, A55, A58, INCPROJ:def_13; A88: t on O by A87, INCSP_1:2; A89: s on O by A87, INCSP_1:2; A90: r on O by A87, INCSP_1:2; A91: now__::_thesis:_(_r_<>_s_implies_b,c_//_b9,c9_) assume A92: r <> s ; ::_thesis: b,c // b9,c9 ex X being Subset of AS st ( O = [(PDir X),2] & X is being_plane ) proof reconsider x = LDir (Line (a,b)), y = LDir (Line (a,c)) as Element of the Points of (ProjHorizon AS) by A33, A31, Th14; A93: [y,O] in the Inc of (IncProjSp_of AS) by A90, INCSP_1:def_1; [x,O] in the Inc of (IncProjSp_of AS) by A89, INCSP_1:def_1; then consider Z9 being Element of the Lines of (ProjHorizon AS) such that A94: O = [Z9,2] by A92, A93, Th41; consider X being Subset of AS such that A95: Z9 = PDir X and A96: X is being_plane by Th15; take X ; ::_thesis: ( O = [(PDir X),2] & X is being_plane ) thus ( O = [(PDir X),2] & X is being_plane ) by A94, A95, A96; ::_thesis: verum end; then t is not Element of AS by A88, Th27; then consider Y being Subset of AS such that A97: t = LDir Y and A98: Y is being_line by Th20; Y '||' Line (b9,c9) by A28, A79, A97, A98, Th28; then A99: Y // Line (b9,c9) by A28, A98, AFF_4:40; Y '||' Line (b,c) by A29, A78, A97, A98, Th28; then Y // Line (b,c) by A29, A98, AFF_4:40; then Line (b,c) // Line (b9,c9) by A99, AFF_1:44; hence b,c // b9,c9 by A76, A38, A69, A71, AFF_1:39; ::_thesis: verum end; now__::_thesis:_(_r_=_s_implies_b,c_//_b9,c9_) assume r = s ; ::_thesis: b,c // b9,c9 then A100: Line (a,b) // Line (a,c) by A33, A31, Th11; then Line (a,b) // Line (a9,c9) by A45, AFF_1:44; then Line (a9,b9) // Line (a9,c9) by A54, AFF_1:44; then A101: c9 in Line (a9,b9) by A52, A43, A41, AFF_1:45; c in Line (a,b) by A82, A65, A67, A100, AFF_1:45; hence b,c // b9,c9 by A85, A50, A54, A101, AFF_1:39; ::_thesis: verum end; hence b,c // b9,c9 by A91; ::_thesis: verum end; hence b,c // b9,c9 by A2, A3, A4, A5, A6, A7, A8, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, Th50; ::_thesis: verum end; hence b,c // b9,c9 by A10, A11, A12, A13, A15, AFF_1:51; ::_thesis: verum end; hence AS is Desarguesian by AFF_2:def_4; ::_thesis: verum end; theorem :: AFPROJ:52 for AS being AffinSpace st IncProjSp_of AS is Fanoian holds AS is Fanoian proof let AS be AffinSpace; ::_thesis: ( IncProjSp_of AS is Fanoian implies AS is Fanoian ) set XX = IncProjSp_of AS; assume A1: IncProjSp_of AS is Fanoian ; ::_thesis: AS is Fanoian for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds a,b // a,c proof let a, b, c, d be Element of AS; ::_thesis: ( a,b // c,d & a,c // b,d & a,d // b,c implies a,b // a,c ) assume that A2: a,b // c,d and A3: a,c // b,d and A4: a,d // b,c ; ::_thesis: a,b // a,c assume A5: not a,b // a,c ; ::_thesis: contradiction then A6: a <> d by A2, AFF_1:4; then A7: Line (a,d) is being_line by AFF_1:def_3; A8: now__::_thesis:_not_b_=_d assume b = d ; ::_thesis: contradiction then b,a // b,c by A2, AFF_1:4; then LIN b,a,c by AFF_1:def_1; then LIN a,b,c by AFF_1:6; hence contradiction by A5, AFF_1:def_1; ::_thesis: verum end; then A9: Line (b,d) is being_line by AFF_1:def_3; A10: now__::_thesis:_not_c_=_d assume c = d ; ::_thesis: contradiction then c,a // c,b by A3, AFF_1:4; then LIN c,a,b by AFF_1:def_1; then LIN a,b,c by AFF_1:6; hence contradiction by A5, AFF_1:def_1; ::_thesis: verum end; then A11: Line (c,d) is being_line by AFF_1:def_3; A12: a <> c by A5, AFF_1:3; then A13: Line (a,c) is being_line by AFF_1:def_3; A14: a <> b by A5, AFF_1:3; then A15: Line (a,b) is being_line by AFF_1:def_3; then reconsider a9 = LDir (Line (a,b)), b9 = LDir (Line (a,c)), c9 = LDir (Line (a,d)) as Element of the Points of (IncProjSp_of AS) by A13, A7, Th20; A16: b <> c by A5, AFF_1:2; then A17: Line (b,c) is being_line by AFF_1:def_3; then reconsider L1 = [(Line (a,b)),1], Q1 = [(Line (c,d)),1], R1 = [(Line (b,d)),1], S1 = [(Line (a,c)),1], A1 = [(Line (a,d)),1], B1 = [(Line (b,c)),1] as Element of the Lines of (IncProjSp_of AS) by A15, A11, A9, A13, A7, Th23; reconsider p = a, q = d, r = c, s = b as Element of the Points of (IncProjSp_of AS) by Th20; A18: a9 on L1 by A15, Th30; c in Line (b,c) by AFF_1:15; then A19: r on B1 by A17, Th26; b in Line (b,c) by AFF_1:15; then A20: s on B1 by A17, Th26; Line (a,d) // Line (b,c) by A4, A16, A6, AFF_1:37; then Line (a,d) '||' Line (b,c) by A7, A17, AFF_4:40; then c9 on B1 by A7, A17, Th28; then A21: {c9,r,s} on B1 by A19, A20, INCSP_1:2; A22: d in Line (b,d) by AFF_1:15; then A23: q on R1 by A9, Th26; A24: c in Line (a,c) by AFF_1:15; then A25: r on S1 by A13, Th26; A26: b9 on S1 by A13, Th30; A27: a in Line (a,c) by AFF_1:15; then p on S1 by A13, Th26; then A28: {b9,p,r} on S1 by A25, A26, INCSP_1:2; A29: Line (a,c) // Line (b,d) by A3, A12, A8, AFF_1:37; then Line (a,c) '||' Line (b,d) by A9, A13, AFF_4:40; then A30: b9 on R1 by A9, A13, Th28; A31: b in Line (b,d) by AFF_1:15; then s on R1 by A9, Th26; then A32: {b9,q,s} on R1 by A23, A30, INCSP_1:2; A33: now__::_thesis:_not_Line_(a,c)_=_Line_(b,d) assume Line (a,c) = Line (b,d) ; ::_thesis: contradiction then LIN a,c,b by A31, AFF_1:def_2; then LIN a,b,c by AFF_1:6; hence contradiction by A5, AFF_1:def_1; ::_thesis: verum end; A34: now__::_thesis:_(_not_q_on_S1_&_not_s_on_S1_) assume ( q on S1 or s on S1 ) ; ::_thesis: contradiction then ( d in Line (a,c) or b in Line (a,c) ) by Th26; hence contradiction by A31, A22, A33, A29, AFF_1:45; ::_thesis: verum end; A35: now__::_thesis:_(_not_p_on_R1_&_not_r_on_R1_) assume ( p on R1 or r on R1 ) ; ::_thesis: contradiction then ( a in Line (b,d) or c in Line (b,d) ) by Th26; hence contradiction by A27, A24, A33, A29, AFF_1:45; ::_thesis: verum end; A36: a in Line (a,b) by AFF_1:15; then consider Y being Subset of AS such that A37: Line (a,b) c= Y and A38: Line (a,c) c= Y and A39: Y is being_plane by A27, A15, A13, AFF_4:38; reconsider C1 = [(PDir Y),2] as Element of the Lines of (IncProjSp_of AS) by A39, Th23; A40: b9 on C1 by A13, A38, A39, Th31; A41: Line (a,b) // Line (c,d) by A2, A14, A10, AFF_1:37; then Line (a,b) '||' Line (c,d) by A15, A11, AFF_4:40; then A42: a9 on Q1 by A15, A11, Th28; d in Line (a,d) by AFF_1:15; then A43: q on A1 by A7, Th26; a in Line (a,d) by AFF_1:15; then A44: p on A1 by A7, Th26; c9 on A1 by A7, Th30; then A45: {c9,p,q} on A1 by A44, A43, INCSP_1:2; A46: b in Line (a,b) by AFF_1:15; then A47: s on L1 by A15, Th26; a9 on C1 by A15, A37, A39, Th31; then A48: {a9,b9} on C1 by A40, INCSP_1:1; A49: d in Line (c,d) by AFF_1:15; then A50: q on Q1 by A11, Th26; A51: c in Line (c,d) by AFF_1:15; then r on Q1 by A11, Th26; then A52: {a9,q,r} on Q1 by A50, A42, INCSP_1:2; A53: now__::_thesis:_not_Line_(a,b)_=_Line_(c,d) assume Line (a,b) = Line (c,d) ; ::_thesis: contradiction then LIN a,b,c by A51, AFF_1:def_2; hence contradiction by A5, AFF_1:def_1; ::_thesis: verum end; A54: now__::_thesis:_(_not_q_on_L1_&_not_r_on_L1_) assume ( q on L1 or r on L1 ) ; ::_thesis: contradiction then ( d in Line (a,b) or c in Line (a,b) ) by Th26; hence contradiction by A51, A49, A53, A41, AFF_1:45; ::_thesis: verum end; A55: now__::_thesis:_(_not_p_on_Q1_&_not_s_on_Q1_) assume ( p on Q1 or s on Q1 ) ; ::_thesis: contradiction then ( a in Line (c,d) or b in Line (c,d) ) by Th26; hence contradiction by A36, A46, A53, A41, AFF_1:45; ::_thesis: verum end; Line (b,d) = b * (Line (a,c)) by A31, A13, A29, AFF_4:def_3; then Line (b,d) c= Y by A46, A13, A37, A38, A39, AFF_4:28; then A56: c9 on C1 by A36, A22, A6, A7, A37, A39, Th31, AFF_4:19; p on L1 by A36, A15, Th26; then {a9,p,s} on L1 by A47, A18, INCSP_1:2; hence contradiction by A1, A56, A54, A34, A55, A35, A52, A32, A28, A45, A21, A48, INCPROJ:def_12; ::_thesis: verum end; hence AS is Fanoian by PAPDESAF:def_1; ::_thesis: verum end;