:: PROJPL_1 semantic presentation begin notation let G be IncProjStr ; let a be POINT of G; let P be LINE of G; antonym a |' P for a on P; end; definition let G be IncProjStr ; let a, b be POINT of G; let P be LINE of G; preda,b |' P means :Def1: :: PROJPL_1:def 1 ( a |' P & b |' P ); end; :: deftheorem Def1 defines |' PROJPL_1:def_1_:_ for G being IncProjStr for a, b being POINT of G for P being LINE of G holds ( a,b |' P iff ( a |' P & b |' P ) ); definition let G be IncProjStr ; let a be POINT of G; let P, Q be LINE of G; preda on P,Q means :Def2: :: PROJPL_1:def 2 ( a on P & a on Q ); end; :: deftheorem Def2 defines on PROJPL_1:def_2_:_ for G being IncProjStr for a being POINT of G for P, Q being LINE of G holds ( a on P,Q iff ( a on P & a on Q ) ); definition let G be IncProjStr ; let a be POINT of G; let P, Q, R be LINE of G; preda on P,Q,R means :Def3: :: PROJPL_1:def 3 ( a on P & a on Q & a on R ); end; :: deftheorem Def3 defines on PROJPL_1:def_3_:_ for G being IncProjStr for a being POINT of G for P, Q, R being LINE of G holds ( a on P,Q,R iff ( a on P & a on Q & a on R ) ); theorem Th1: :: PROJPL_1:1 for G being IncProjStr for a, b, c being POINT of G for P, Q, R being LINE of G holds ( ( {a,b} on P implies {b,a} on P ) & ( {a,b,c} on P implies ( {a,c,b} on P & {b,a,c} on P & {b,c,a} on P & {c,a,b} on P & {c,b,a} on P ) ) & ( a on P,Q implies a on Q,P ) & ( a on P,Q,R implies ( a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P ) ) ) proof let G be IncProjStr ; ::_thesis: for a, b, c being POINT of G for P, Q, R being LINE of G holds ( ( {a,b} on P implies {b,a} on P ) & ( {a,b,c} on P implies ( {a,c,b} on P & {b,a,c} on P & {b,c,a} on P & {c,a,b} on P & {c,b,a} on P ) ) & ( a on P,Q implies a on Q,P ) & ( a on P,Q,R implies ( a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P ) ) ) let a, b, c be POINT of G; ::_thesis: for P, Q, R being LINE of G holds ( ( {a,b} on P implies {b,a} on P ) & ( {a,b,c} on P implies ( {a,c,b} on P & {b,a,c} on P & {b,c,a} on P & {c,a,b} on P & {c,b,a} on P ) ) & ( a on P,Q implies a on Q,P ) & ( a on P,Q,R implies ( a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P ) ) ) let P, Q, R be LINE of G; ::_thesis: ( ( {a,b} on P implies {b,a} on P ) & ( {a,b,c} on P implies ( {a,c,b} on P & {b,a,c} on P & {b,c,a} on P & {c,a,b} on P & {c,b,a} on P ) ) & ( a on P,Q implies a on Q,P ) & ( a on P,Q,R implies ( a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P ) ) ) thus ( {a,b} on P implies {b,a} on P ) ; ::_thesis: ( ( {a,b,c} on P implies ( {a,c,b} on P & {b,a,c} on P & {b,c,a} on P & {c,a,b} on P & {c,b,a} on P ) ) & ( a on P,Q implies a on Q,P ) & ( a on P,Q,R implies ( a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P ) ) ) thus ( {a,b,c} on P implies ( {a,c,b} on P & {b,a,c} on P & {b,c,a} on P & {c,a,b} on P & {c,b,a} on P ) ) ::_thesis: ( ( a on P,Q implies a on Q,P ) & ( a on P,Q,R implies ( a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P ) ) ) proof assume A1: {a,b,c} on P ; ::_thesis: ( {a,c,b} on P & {b,a,c} on P & {b,c,a} on P & {c,a,b} on P & {c,b,a} on P ) then A2: c on P by INCSP_1:2; ( a on P & b on P ) by A1, INCSP_1:2; hence ( {a,c,b} on P & {b,a,c} on P & {b,c,a} on P & {c,a,b} on P & {c,b,a} on P ) by A2, INCSP_1:2; ::_thesis: verum end; thus ( a on P,Q implies a on Q,P ) ::_thesis: ( a on P,Q,R implies ( a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P ) ) proof assume a on P,Q ; ::_thesis: a on Q,P then ( a on P & a on Q ) by Def2; hence a on Q,P by Def2; ::_thesis: verum end; assume A3: a on P,Q,R ; ::_thesis: ( a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P ) then A4: a on R by Def3; ( a on P & a on Q ) by A3, Def3; hence ( a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P ) by A4, Def3; ::_thesis: verum end; definition let IT be IncProjStr ; attrIT is configuration means :Def4: :: PROJPL_1:def 4 for p, q being POINT of IT for P, Q being LINE of IT st p on P & q on P & p on Q & q on Q & not p = q holds P = Q; end; :: deftheorem Def4 defines configuration PROJPL_1:def_4_:_ for IT being IncProjStr holds ( IT is configuration iff for p, q being POINT of IT for P, Q being LINE of IT st p on P & q on P & p on Q & q on Q & not p = q holds P = Q ); theorem Th2: :: PROJPL_1:2 for G being IncProjStr holds ( G is configuration iff for p, q being POINT of G for P, Q being LINE of G st {p,q} on P & {p,q} on Q & not p = q holds P = Q ) proof let G be IncProjStr ; ::_thesis: ( G is configuration iff for p, q being POINT of G for P, Q being LINE of G st {p,q} on P & {p,q} on Q & not p = q holds P = Q ) hereby ::_thesis: ( ( for p, q being POINT of G for P, Q being LINE of G st {p,q} on P & {p,q} on Q & not p = q holds P = Q ) implies G is configuration ) assume A1: G is configuration ; ::_thesis: for p, q being POINT of G for P, Q being LINE of G st {p,q} on P & {p,q} on Q & not p = q holds P = Q let p, q be POINT of G; ::_thesis: for P, Q being LINE of G st {p,q} on P & {p,q} on Q & not p = q holds P = Q let P, Q be LINE of G; ::_thesis: ( {p,q} on P & {p,q} on Q & not p = q implies P = Q ) assume that A2: {p,q} on P and A3: {p,q} on Q ; ::_thesis: ( p = q or P = Q ) A4: ( p on Q & q on Q ) by A3, INCSP_1:1; ( p on P & q on P ) by A2, INCSP_1:1; hence ( p = q or P = Q ) by A1, A4, Def4; ::_thesis: verum end; hereby ::_thesis: verum assume A5: for p, q being POINT of G for P, Q being LINE of G st {p,q} on P & {p,q} on Q & not p = q holds P = Q ; ::_thesis: G is configuration now__::_thesis:_for_p,_q_being_POINT_of_G for_P,_Q_being_LINE_of_G_st_p_on_P_&_q_on_P_&_p_on_Q_&_q_on_Q_&_not_p_=_q_holds_ P_=_Q let p, q be POINT of G; ::_thesis: for P, Q being LINE of G st p on P & q on P & p on Q & q on Q & not p = q holds P = Q let P, Q be LINE of G; ::_thesis: ( p on P & q on P & p on Q & q on Q & not p = q implies P = Q ) assume ( p on P & q on P & p on Q & q on Q ) ; ::_thesis: ( p = q or P = Q ) then ( {p,q} on P & {p,q} on Q ) by INCSP_1:1; hence ( p = q or P = Q ) by A5; ::_thesis: verum end; hence G is configuration by Def4; ::_thesis: verum end; end; theorem Th3: :: PROJPL_1:3 for G being IncProjStr holds ( G is configuration iff for p, q being POINT of G for P, Q being LINE of G st p on P,Q & q on P,Q & not p = q holds P = Q ) proof let G be IncProjStr ; ::_thesis: ( G is configuration iff for p, q being POINT of G for P, Q being LINE of G st p on P,Q & q on P,Q & not p = q holds P = Q ) hereby ::_thesis: ( ( for p, q being POINT of G for P, Q being LINE of G st p on P,Q & q on P,Q & not p = q holds P = Q ) implies G is configuration ) assume A1: G is configuration ; ::_thesis: for p, q being POINT of G for P, Q being LINE of G st p on P,Q & q on P,Q & not p = q holds P = Q let p, q be POINT of G; ::_thesis: for P, Q being LINE of G st p on P,Q & q on P,Q & not p = q holds P = Q let P, Q be LINE of G; ::_thesis: ( p on P,Q & q on P,Q & not p = q implies P = Q ) assume A2: ( p on P,Q & q on P,Q ) ; ::_thesis: ( p = q or P = Q ) then A3: ( p on Q & q on Q ) by Def2; ( p on P & q on P ) by A2, Def2; hence ( p = q or P = Q ) by A1, A3, Def4; ::_thesis: verum end; hereby ::_thesis: verum assume A4: for p, q being POINT of G for P, Q being LINE of G st p on P,Q & q on P,Q & not p = q holds P = Q ; ::_thesis: G is configuration now__::_thesis:_for_p,_q_being_POINT_of_G for_P,_Q_being_LINE_of_G_st_p_on_P_&_q_on_P_&_p_on_Q_&_q_on_Q_&_not_p_=_q_holds_ P_=_Q let p, q be POINT of G; ::_thesis: for P, Q being LINE of G st p on P & q on P & p on Q & q on Q & not p = q holds P = Q let P, Q be LINE of G; ::_thesis: ( p on P & q on P & p on Q & q on Q & not p = q implies P = Q ) assume ( p on P & q on P & p on Q & q on Q ) ; ::_thesis: ( p = q or P = Q ) then ( p on P,Q & q on P,Q ) by Def2; hence ( p = q or P = Q ) by A4; ::_thesis: verum end; hence G is configuration by Def4; ::_thesis: verum end; end; theorem Th4: :: PROJPL_1:4 for G being IncProjStr holds ( G is IncProjSp iff ( G is configuration & ( for p, q being POINT of G ex P being LINE of G st {p,q} on P ) & ex p being POINT of G ex P being LINE of G st p |' P & ( for P being LINE of G ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) ) & ( for a, b, c, d, p being POINT of G for M, N, P, Q being LINE of G st {a,b,p} on M & {c,d,p} on N & {a,c} on P & {b,d} on Q & p |' P & p |' Q & M <> N holds ex q being POINT of G st q on P,Q ) ) ) proof let G be IncProjStr ; ::_thesis: ( G is IncProjSp iff ( G is configuration & ( for p, q being POINT of G ex P being LINE of G st {p,q} on P ) & ex p being POINT of G ex P being LINE of G st p |' P & ( for P being LINE of G ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) ) & ( for a, b, c, d, p being POINT of G for M, N, P, Q being LINE of G st {a,b,p} on M & {c,d,p} on N & {a,c} on P & {b,d} on Q & p |' P & p |' Q & M <> N holds ex q being POINT of G st q on P,Q ) ) ) hereby ::_thesis: ( G is configuration & ( for p, q being POINT of G ex P being LINE of G st {p,q} on P ) & ex p being POINT of G ex P being LINE of G st p |' P & ( for P being LINE of G ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) ) & ( for a, b, c, d, p being POINT of G for M, N, P, Q being LINE of G st {a,b,p} on M & {c,d,p} on N & {a,c} on P & {b,d} on Q & p |' P & p |' Q & M <> N holds ex q being POINT of G st q on P,Q ) implies G is IncProjSp ) assume A1: G is IncProjSp ; ::_thesis: ( G is configuration & ( for p, q being POINT of G ex P being LINE of G st {p,q} on P ) & ex p being POINT of G ex P being LINE of G st p |' P & ( for P being LINE of G ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) ) & ( for a, b, c, d, p being POINT of G for M, N, P, Q being LINE of G st {a,b,p} on M & {c,d,p} on N & {a,c} on P & {b,d} on Q & p |' P & p |' Q & M <> N holds ex q being POINT of G st q on P,Q ) ) then for p, q being POINT of G for P, Q being LINE of G st p on P & q on P & p on Q & q on Q & not p = q holds P = Q by INCPROJ:def_4; hence G is configuration by Def4; ::_thesis: ( ( for p, q being POINT of G ex P being LINE of G st {p,q} on P ) & ex p being POINT of G ex P being LINE of G st p |' P & ( for P being LINE of G ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) ) & ( for a, b, c, d, p being POINT of G for M, N, P, Q being LINE of G st {a,b,p} on M & {c,d,p} on N & {a,c} on P & {b,d} on Q & p |' P & p |' Q & M <> N holds ex q being POINT of G st q on P,Q ) ) thus for p, q being POINT of G ex P being LINE of G st {p,q} on P ::_thesis: ( ex p being POINT of G ex P being LINE of G st p |' P & ( for P being LINE of G ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) ) & ( for a, b, c, d, p being POINT of G for M, N, P, Q being LINE of G st {a,b,p} on M & {c,d,p} on N & {a,c} on P & {b,d} on Q & p |' P & p |' Q & M <> N holds ex q being POINT of G st q on P,Q ) ) proof let p, q be POINT of G; ::_thesis: ex P being LINE of G st {p,q} on P consider P being LINE of G such that A2: ( p on P & q on P ) by A1, INCPROJ:def_5; take P ; ::_thesis: {p,q} on P thus {p,q} on P by A2, INCSP_1:1; ::_thesis: verum end; thus ex p being POINT of G ex P being LINE of G st p |' P by A1, INCPROJ:def_6; ::_thesis: ( ( for P being LINE of G ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) ) & ( for a, b, c, d, p being POINT of G for M, N, P, Q being LINE of G st {a,b,p} on M & {c,d,p} on N & {a,c} on P & {b,d} on Q & p |' P & p |' Q & M <> N holds ex q being POINT of G st q on P,Q ) ) thus for P being LINE of G ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) ::_thesis: for a, b, c, d, p being POINT of G for M, N, P, Q being LINE of G st {a,b,p} on M & {c,d,p} on N & {a,c} on P & {b,d} on Q & p |' P & p |' Q & M <> N holds ex q being POINT of G st q on P,Q proof let P be LINE of G; ::_thesis: ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) consider a, b, c being POINT of G such that A3: ( a <> b & b <> c & c <> a ) and A4: ( a on P & b on P & c on P ) by A1, INCPROJ:def_7; take a ; ::_thesis: ex b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) take b ; ::_thesis: ex c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) take c ; ::_thesis: ( a,b,c are_mutually_different & {a,b,c} on P ) thus a,b,c are_mutually_different by A3, ZFMISC_1:def_5; ::_thesis: {a,b,c} on P thus {a,b,c} on P by A4, INCSP_1:2; ::_thesis: verum end; thus for a, b, c, d, p being POINT of G for M, N, P, Q being LINE of G st {a,b,p} on M & {c,d,p} on N & {a,c} on P & {b,d} on Q & p |' P & p |' Q & M <> N holds ex q being POINT of G st q on P,Q ::_thesis: verum proof let a, b, c, d, p be POINT of G; ::_thesis: for M, N, P, Q being LINE of G st {a,b,p} on M & {c,d,p} on N & {a,c} on P & {b,d} on Q & p |' P & p |' Q & M <> N holds ex q being POINT of G st q on P,Q let M, N, P, Q be LINE of G; ::_thesis: ( {a,b,p} on M & {c,d,p} on N & {a,c} on P & {b,d} on Q & p |' P & p |' Q & M <> N implies ex q being POINT of G st q on P,Q ) assume that A5: {a,b,p} on M and A6: {c,d,p} on N and A7: {a,c} on P and A8: {b,d} on Q and A9: ( p |' P & p |' Q & M <> N ) ; ::_thesis: ex q being POINT of G st q on P,Q A10: ( a on M & b on M ) by A5, INCSP_1:2; A11: ( a on P & c on P ) by A7, INCSP_1:1; A12: ( d on N & p on N ) by A6, INCSP_1:2; A13: ( b on Q & d on Q ) by A8, INCSP_1:1; ( p on M & c on N ) by A5, A6, INCSP_1:2; then consider q being POINT of G such that A14: ( q on P & q on Q ) by A1, A9, A10, A12, A11, A13, INCPROJ:def_8; take q ; ::_thesis: q on P,Q thus q on P,Q by A14, Def2; ::_thesis: verum end; end; hereby ::_thesis: verum assume that A15: G is configuration and A16: for p, q being POINT of G ex P being LINE of G st {p,q} on P and A17: ex p being POINT of G ex P being LINE of G st p |' P and A18: for P being LINE of G ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) and A19: for a, b, c, d, p being POINT of G for M, N, P, Q being LINE of G st {a,b,p} on M & {c,d,p} on N & {a,c} on P & {b,d} on Q & p |' P & p |' Q & M <> N holds ex q being POINT of G st q on P,Q ; ::_thesis: G is IncProjSp A20: now__::_thesis:_for_p,_q_being_POINT_of_G_ex_P_being_LINE_of_G_st_ (_p_on_P_&_q_on_P_) let p, q be POINT of G; ::_thesis: ex P being LINE of G st ( p on P & q on P ) consider P being LINE of G such that A21: {p,q} on P by A16; take P = P; ::_thesis: ( p on P & q on P ) thus ( p on P & q on P ) by A21, INCSP_1:1; ::_thesis: verum end; A22: now__::_thesis:_for_P_being_LINE_of_G_ex_a,_b,_c_being_POINT_of_G_st_ (_a_<>_b_&_b_<>_c_&_c_<>_a_&_a_on_P_&_b_on_P_&_c_on_P_) let P be LINE of G; ::_thesis: ex a, b, c being POINT of G st ( a <> b & b <> c & c <> a & a on P & b on P & c on P ) consider a, b, c being POINT of G such that A23: a,b,c are_mutually_different and A24: {a,b,c} on P by A18; A25: ( a <> b & b <> c ) by A23, ZFMISC_1:def_5; A26: ( b on P & c on P ) by A24, INCSP_1:2; ( c <> a & a on P ) by A23, A24, INCSP_1:2, ZFMISC_1:def_5; hence ex a, b, c being POINT of G st ( a <> b & b <> c & c <> a & a on P & b on P & c on P ) by A25, A26; ::_thesis: verum end; A27: for a, b, c, d, p, q being POINT of G for M, N, P, Q being LINE of G 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 G st ( q on P & q on Q ) proof let a, b, c, d, p, q be POINT of G; ::_thesis: for M, N, P, Q being LINE of G 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 G st ( q on P & q on Q ) let M, N, P, Q be LINE of G; ::_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 G st ( q on P & q on Q ) ) assume that A28: ( a on M & b on M & c on N & d on N & p on M & p on N ) and A29: ( a on P & c on P & b on Q & d on Q ) and A30: ( not p on P & not p on Q & M <> N ) ; ::_thesis: ex q being POINT of G st ( q on P & q on Q ) A31: ( {a,c} on P & {b,d} on Q ) by A29, INCSP_1:1; ( {a,b,p} on M & {c,d,p} on N ) by A28, INCSP_1:2; then consider q1 being POINT of G such that A32: q1 on P,Q by A19, A30, A31; take q1 ; ::_thesis: ( q1 on P & q1 on Q ) thus ( q1 on P & q1 on Q ) by A32, Def2; ::_thesis: verum end; for p, q being POINT of G for P, Q being LINE of G st p on P & q on P & p on Q & q on Q & not p = q holds P = Q by A15, Def4; hence G is IncProjSp by A17, A20, A22, A27, INCPROJ:def_4, INCPROJ:def_5, INCPROJ:def_6, INCPROJ:def_7, INCPROJ:def_8; ::_thesis: verum end; end; definition mode IncProjectivePlane is 2-dimensional IncProjSp; end; definition let G be IncProjStr ; let a, b, c be POINT of G; preda,b,c is_collinear means :Def5: :: PROJPL_1:def 5 ex P being LINE of G st {a,b,c} on P; end; :: deftheorem Def5 defines is_collinear PROJPL_1:def_5_:_ for G being IncProjStr for a, b, c being POINT of G holds ( a,b,c is_collinear iff ex P being LINE of G st {a,b,c} on P ); notation let G be IncProjStr ; let a, b, c be POINT of G; antonym a,b,c is_a_triangle for a,b,c is_collinear ; end; theorem Th5: :: PROJPL_1:5 for G being IncProjStr for a, b, c being POINT of G holds ( a,b,c is_collinear iff ex P being LINE of G st ( a on P & b on P & c on P ) ) proof let G be IncProjStr ; ::_thesis: for a, b, c being POINT of G holds ( a,b,c is_collinear iff ex P being LINE of G st ( a on P & b on P & c on P ) ) let a, b, c be POINT of G; ::_thesis: ( a,b,c is_collinear iff ex P being LINE of G st ( a on P & b on P & c on P ) ) ( ex P being LINE of G st {a,b,c} on P iff ex P being LINE of G st ( a on P & b on P & c on P ) ) proof hereby ::_thesis: ( ex P being LINE of G st ( a on P & b on P & c on P ) implies ex P being LINE of G st {a,b,c} on P ) given P being LINE of G such that A1: {a,b,c} on P ; ::_thesis: ex P being LINE of G st ( a on P & b on P & c on P ) take P = P; ::_thesis: ( a on P & b on P & c on P ) thus ( a on P & b on P & c on P ) by A1, INCSP_1:2; ::_thesis: verum end; hereby ::_thesis: verum given P being LINE of G such that A2: ( a on P & b on P & c on P ) ; ::_thesis: ex P being LINE of G st {a,b,c} on P take P = P; ::_thesis: {a,b,c} on P thus {a,b,c} on P by A2, INCSP_1:2; ::_thesis: verum end; end; hence ( a,b,c is_collinear iff ex P being LINE of G st ( a on P & b on P & c on P ) ) by Def5; ::_thesis: verum end; theorem :: PROJPL_1:6 for G being IncProjStr for a, b, c being POINT of G holds ( a,b,c is_a_triangle iff for P being LINE of G holds ( a |' P or b |' P or c |' P ) ) by Th5; definition let G be IncProjStr ; let a, b, c, d be POINT of G; preda,b,c,d is_a_quadrangle means :Def6: :: PROJPL_1:def 6 ( a,b,c is_a_triangle & b,c,d is_a_triangle & c,d,a is_a_triangle & d,a,b is_a_triangle ); end; :: deftheorem Def6 defines is_a_quadrangle PROJPL_1:def_6_:_ for G being IncProjStr for a, b, c, d being POINT of G holds ( a,b,c,d is_a_quadrangle iff ( a,b,c is_a_triangle & b,c,d is_a_triangle & c,d,a is_a_triangle & d,a,b is_a_triangle ) ); theorem Th7: :: PROJPL_1:7 for G being IncProjStr st G is IncProjSp holds ex A, B being LINE of G st A <> B proof let G be IncProjStr ; ::_thesis: ( G is IncProjSp implies ex A, B being LINE of G st A <> B ) set a = the POINT of G; assume G is IncProjSp ; ::_thesis: ex A, B being LINE of G st A <> B then consider A, B, C being LINE of G such that the POINT of G on A and the POINT of G on B and the POINT of G on C and A1: A <> B and B <> C and C <> A by PROJRED1:5; take A ; ::_thesis: ex B being LINE of G st A <> B take B ; ::_thesis: A <> B thus A <> B by A1; ::_thesis: verum end; theorem Th8: :: PROJPL_1:8 for G being IncProjStr for a being POINT of G for A being LINE of G st G is IncProjSp holds ex b, c being POINT of G st ( {b,c} on A & a,b,c are_mutually_different ) proof let G be IncProjStr ; ::_thesis: for a being POINT of G for A being LINE of G st G is IncProjSp holds ex b, c being POINT of G st ( {b,c} on A & a,b,c are_mutually_different ) let a be POINT of G; ::_thesis: for A being LINE of G st G is IncProjSp holds ex b, c being POINT of G st ( {b,c} on A & a,b,c are_mutually_different ) let A be LINE of G; ::_thesis: ( G is IncProjSp implies ex b, c being POINT of G st ( {b,c} on A & a,b,c are_mutually_different ) ) assume A1: G is IncProjSp ; ::_thesis: ex b, c being POINT of G st ( {b,c} on A & a,b,c are_mutually_different ) then consider b being POINT of G such that A2: ( b on A & b <> a ) and b <> a by PROJRED1:8; consider c being POINT of G such that A3: ( c on A & c <> a & c <> b ) by A1, PROJRED1:8; take b ; ::_thesis: ex c being POINT of G st ( {b,c} on A & a,b,c are_mutually_different ) take c ; ::_thesis: ( {b,c} on A & a,b,c are_mutually_different ) thus ( {b,c} on A & a,b,c are_mutually_different ) by A2, A3, INCSP_1:1, ZFMISC_1:def_5; ::_thesis: verum end; theorem Th9: :: PROJPL_1:9 for G being IncProjStr for a being POINT of G for A, B being LINE of G st G is IncProjSp & A <> B holds ex b being POINT of G st ( b on A & b |' B & a <> b ) proof let G be IncProjStr ; ::_thesis: for a being POINT of G for A, B being LINE of G st G is IncProjSp & A <> B holds ex b being POINT of G st ( b on A & b |' B & a <> b ) let a be POINT of G; ::_thesis: for A, B being LINE of G st G is IncProjSp & A <> B holds ex b being POINT of G st ( b on A & b |' B & a <> b ) let A, B be LINE of G; ::_thesis: ( G is IncProjSp & A <> B implies ex b being POINT of G st ( b on A & b |' B & a <> b ) ) assume that A1: G is IncProjSp and A2: A <> B ; ::_thesis: ex b being POINT of G st ( b on A & b |' B & a <> b ) consider b, c being POINT of G such that A3: {b,c} on A and A4: a,b,c are_mutually_different by A1, Th8; A5: a <> c by A4, ZFMISC_1:def_5; A6: c on A by A3, INCSP_1:1; A7: b <> c by A4, ZFMISC_1:def_5; A8: b on A by A3, INCSP_1:1; A9: a <> b by A4, ZFMISC_1:def_5; now__::_thesis:_(_(_b_|'_B_&_ex_b_being_POINT_of_G_st_ (_b_on_A_&_b_|'_B_&_a_<>_b_)_)_or_(_c_|'_B_&_ex_b_being_POINT_of_G_st_ (_b_on_A_&_b_|'_B_&_a_<>_b_)_)_) percases ( b |' B or c |' B ) by A1, A2, A7, A8, A6, INCPROJ:def_4; case b |' B ; ::_thesis: ex b being POINT of G st ( b on A & b |' B & a <> b ) hence ex b being POINT of G st ( b on A & b |' B & a <> b ) by A9, A8; ::_thesis: verum end; case c |' B ; ::_thesis: ex b being POINT of G st ( b on A & b |' B & a <> b ) hence ex b being POINT of G st ( b on A & b |' B & a <> b ) by A5, A6; ::_thesis: verum end; end; end; hence ex b being POINT of G st ( b on A & b |' B & a <> b ) ; ::_thesis: verum end; theorem Th10: :: PROJPL_1:10 for G being IncProjStr for a1, a2, b being POINT of G for A being LINE of G st G is configuration & {a1,a2} on A & a1 <> a2 & b |' A holds a1,a2,b is_a_triangle proof let G be IncProjStr ; ::_thesis: for a1, a2, b being POINT of G for A being LINE of G st G is configuration & {a1,a2} on A & a1 <> a2 & b |' A holds a1,a2,b is_a_triangle let a1, a2, b be POINT of G; ::_thesis: for A being LINE of G st G is configuration & {a1,a2} on A & a1 <> a2 & b |' A holds a1,a2,b is_a_triangle let A be LINE of G; ::_thesis: ( G is configuration & {a1,a2} on A & a1 <> a2 & b |' A implies a1,a2,b is_a_triangle ) assume that A1: G is configuration and A2: {a1,a2} on A and A3: ( a1 <> a2 & b |' A ) and A4: a1,a2,b is_collinear ; ::_thesis: contradiction A5: ( a1 on A & a2 on A ) by A2, INCSP_1:1; ex P being LINE of G st ( a1 on P & a2 on P & b on P ) by A4, Th5; hence contradiction by A1, A3, A5, Def4; ::_thesis: verum end; theorem Th11: :: PROJPL_1:11 for G being IncProjStr for a, b, c being POINT of G st a,b,c is_collinear holds ( a,c,b is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear & c,b,a is_collinear ) proof let G be IncProjStr ; ::_thesis: for a, b, c being POINT of G st a,b,c is_collinear holds ( a,c,b is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear & c,b,a is_collinear ) let a, b, c be POINT of G; ::_thesis: ( a,b,c is_collinear implies ( a,c,b is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear & c,b,a is_collinear ) ) assume a,b,c is_collinear ; ::_thesis: ( a,c,b is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear & c,b,a is_collinear ) then consider P being LINE of G such that A1: {a,b,c} on P by Def5; A2: {c,b,a} on P by A1, Th1; A3: ( {b,c,a} on P & {c,a,b} on P ) by A1, Th1; ( {a,c,b} on P & {b,a,c} on P ) by A1, Th1; hence ( a,c,b is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear & c,b,a is_collinear ) by A3, A2, Def5; ::_thesis: verum end; theorem :: PROJPL_1:12 for G being IncProjStr for a, b, c being POINT of G st a,b,c is_a_triangle holds ( a,c,b is_a_triangle & b,a,c is_a_triangle & b,c,a is_a_triangle & c,a,b is_a_triangle & c,b,a is_a_triangle ) by Th11; theorem Th13: :: PROJPL_1:13 for G being IncProjStr for a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle holds ( a,c,b,d is_a_quadrangle & b,a,c,d is_a_quadrangle & b,c,a,d is_a_quadrangle & c,a,b,d is_a_quadrangle & c,b,a,d is_a_quadrangle & a,b,d,c is_a_quadrangle & a,c,d,b is_a_quadrangle & b,a,d,c is_a_quadrangle & b,c,d,a is_a_quadrangle & c,a,d,b is_a_quadrangle & c,b,d,a is_a_quadrangle & a,d,b,c is_a_quadrangle & a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) proof let G be IncProjStr ; ::_thesis: for a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle holds ( a,c,b,d is_a_quadrangle & b,a,c,d is_a_quadrangle & b,c,a,d is_a_quadrangle & c,a,b,d is_a_quadrangle & c,b,a,d is_a_quadrangle & a,b,d,c is_a_quadrangle & a,c,d,b is_a_quadrangle & b,a,d,c is_a_quadrangle & b,c,d,a is_a_quadrangle & c,a,d,b is_a_quadrangle & c,b,d,a is_a_quadrangle & a,d,b,c is_a_quadrangle & a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) let a, b, c, d be POINT of G; ::_thesis: ( a,b,c,d is_a_quadrangle implies ( a,c,b,d is_a_quadrangle & b,a,c,d is_a_quadrangle & b,c,a,d is_a_quadrangle & c,a,b,d is_a_quadrangle & c,b,a,d is_a_quadrangle & a,b,d,c is_a_quadrangle & a,c,d,b is_a_quadrangle & b,a,d,c is_a_quadrangle & b,c,d,a is_a_quadrangle & c,a,d,b is_a_quadrangle & c,b,d,a is_a_quadrangle & a,d,b,c is_a_quadrangle & a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) ) assume A1: a,b,c,d is_a_quadrangle ; ::_thesis: ( a,c,b,d is_a_quadrangle & b,a,c,d is_a_quadrangle & b,c,a,d is_a_quadrangle & c,a,b,d is_a_quadrangle & c,b,a,d is_a_quadrangle & a,b,d,c is_a_quadrangle & a,c,d,b is_a_quadrangle & b,a,d,c is_a_quadrangle & b,c,d,a is_a_quadrangle & c,a,d,b is_a_quadrangle & c,b,d,a is_a_quadrangle & a,d,b,c is_a_quadrangle & a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) then A2: a,b,c is_a_triangle by Def6; then A3: a,c,b is_a_triangle by Th11; A4: c,b,a is_a_triangle by A2, Th11; A5: b,c,a is_a_triangle by A2, Th11; A6: c,a,b is_a_triangle by A2, Th11; A7: b,a,c is_a_triangle by A2, Th11; A8: c,d,a is_a_triangle by A1, Def6; then A9: c,a,d is_a_triangle by Th11; A10: a,d,c is_a_triangle by A8, Th11; A11: d,a,c is_a_triangle by A8, Th11; A12: d,a,b is_a_triangle by A1, Def6; then A13: d,b,a is_a_triangle by Th11; A14: b,a,d is_a_triangle by A12, Th11; A15: a,b,d is_a_triangle by A12, Th11; A16: b,d,a is_a_triangle by A12, Th11; A17: a,d,b is_a_triangle by A12, Th11; A18: b,c,d is_a_triangle by A1, Def6; then A19: c,b,d is_a_triangle by Th11; hence a,c,b,d is_a_quadrangle by A3, A11, A16, Def6; ::_thesis: ( b,a,c,d is_a_quadrangle & b,c,a,d is_a_quadrangle & c,a,b,d is_a_quadrangle & c,b,a,d is_a_quadrangle & a,b,d,c is_a_quadrangle & a,c,d,b is_a_quadrangle & b,a,d,c is_a_quadrangle & b,c,d,a is_a_quadrangle & c,a,d,b is_a_quadrangle & c,b,d,a is_a_quadrangle & a,d,b,c is_a_quadrangle & a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) A20: a,c,d is_a_triangle by A8, Th11; A21: c,d,b is_a_triangle by A18, Th11; hence b,a,c,d is_a_quadrangle by A7, A20, A13, Def6; ::_thesis: ( b,c,a,d is_a_quadrangle & c,a,b,d is_a_quadrangle & c,b,a,d is_a_quadrangle & a,b,d,c is_a_quadrangle & a,c,d,b is_a_quadrangle & b,a,d,c is_a_quadrangle & b,c,d,a is_a_quadrangle & c,a,d,b is_a_quadrangle & c,b,d,a is_a_quadrangle & a,d,b,c is_a_quadrangle & a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) A22: d,b,c is_a_triangle by A18, Th11; hence b,c,a,d is_a_quadrangle by A5, A9, A17, Def6; ::_thesis: ( c,a,b,d is_a_quadrangle & c,b,a,d is_a_quadrangle & a,b,d,c is_a_quadrangle & a,c,d,b is_a_quadrangle & b,a,d,c is_a_quadrangle & b,c,d,a is_a_quadrangle & c,a,d,b is_a_quadrangle & c,b,d,a is_a_quadrangle & a,d,b,c is_a_quadrangle & a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) A23: d,c,a is_a_triangle by A8, Th11; A24: b,d,c is_a_triangle by A18, Th11; hence c,a,b,d is_a_quadrangle by A6, A23, A15, Def6; ::_thesis: ( c,b,a,d is_a_quadrangle & a,b,d,c is_a_quadrangle & a,c,d,b is_a_quadrangle & b,a,d,c is_a_quadrangle & b,c,d,a is_a_quadrangle & c,a,d,b is_a_quadrangle & c,b,d,a is_a_quadrangle & a,d,b,c is_a_quadrangle & a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) A25: d,c,b is_a_triangle by A18, Th11; hence c,b,a,d is_a_quadrangle by A4, A10, A14, Def6; ::_thesis: ( a,b,d,c is_a_quadrangle & a,c,d,b is_a_quadrangle & b,a,d,c is_a_quadrangle & b,c,d,a is_a_quadrangle & c,a,d,b is_a_quadrangle & c,b,d,a is_a_quadrangle & a,d,b,c is_a_quadrangle & a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) thus a,b,d,c is_a_quadrangle by A6, A24, A23, A15, Def6; ::_thesis: ( a,c,d,b is_a_quadrangle & b,a,d,c is_a_quadrangle & b,c,d,a is_a_quadrangle & c,a,d,b is_a_quadrangle & c,b,d,a is_a_quadrangle & a,d,b,c is_a_quadrangle & a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) thus a,c,d,b is_a_quadrangle by A7, A21, A20, A13, Def6; ::_thesis: ( b,a,d,c is_a_quadrangle & b,c,d,a is_a_quadrangle & c,a,d,b is_a_quadrangle & c,b,d,a is_a_quadrangle & a,d,b,c is_a_quadrangle & a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) thus b,a,d,c is_a_quadrangle by A4, A25, A10, A14, Def6; ::_thesis: ( b,c,d,a is_a_quadrangle & c,a,d,b is_a_quadrangle & c,b,d,a is_a_quadrangle & a,d,b,c is_a_quadrangle & a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) thus b,c,d,a is_a_quadrangle by A2, A18, A8, A12, Def6; ::_thesis: ( c,a,d,b is_a_quadrangle & c,b,d,a is_a_quadrangle & a,d,b,c is_a_quadrangle & a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) thus c,a,d,b is_a_quadrangle by A5, A22, A9, A17, Def6; ::_thesis: ( c,b,d,a is_a_quadrangle & a,d,b,c is_a_quadrangle & a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) thus c,b,d,a is_a_quadrangle by A3, A19, A11, A16, Def6; ::_thesis: ( a,d,b,c is_a_quadrangle & a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) thus a,d,b,c is_a_quadrangle by A5, A22, A9, A17, Def6; ::_thesis: ( a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) thus a,d,c,b is_a_quadrangle by A4, A25, A10, A14, Def6; ::_thesis: ( b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) thus b,d,a,c is_a_quadrangle by A3, A19, A11, A16, Def6; ::_thesis: ( b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) thus b,d,c,a is_a_quadrangle by A6, A24, A23, A15, Def6; ::_thesis: ( c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) thus c,d,a,b is_a_quadrangle by A2, A18, A8, A12, Def6; ::_thesis: ( c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) thus c,d,b,a is_a_quadrangle by A7, A21, A20, A13, Def6; ::_thesis: ( d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) thus d,a,b,c is_a_quadrangle by A2, A18, A8, A12, Def6; ::_thesis: ( d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) thus d,a,c,b is_a_quadrangle by A3, A19, A11, A16, Def6; ::_thesis: ( d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) thus d,b,a,c is_a_quadrangle by A7, A21, A20, A13, Def6; ::_thesis: ( d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) thus d,b,c,a is_a_quadrangle by A5, A22, A9, A17, Def6; ::_thesis: ( d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle ) thus d,c,a,b is_a_quadrangle by A6, A24, A23, A15, Def6; ::_thesis: d,c,b,a is_a_quadrangle thus d,c,b,a is_a_quadrangle by A4, A25, A10, A14, Def6; ::_thesis: verum end; theorem Th14: :: PROJPL_1:14 for G being IncProjStr for a1, a2, b1, b2 being POINT of G for A, B being LINE of G st G is configuration & {a1,a2} on A & {b1,b2} on B & a1,a2 |' B & b1,b2 |' A & a1 <> a2 & b1 <> b2 holds a1,a2,b1,b2 is_a_quadrangle proof let G be IncProjStr ; ::_thesis: for a1, a2, b1, b2 being POINT of G for A, B being LINE of G st G is configuration & {a1,a2} on A & {b1,b2} on B & a1,a2 |' B & b1,b2 |' A & a1 <> a2 & b1 <> b2 holds a1,a2,b1,b2 is_a_quadrangle let a1, a2, b1, b2 be POINT of G; ::_thesis: for A, B being LINE of G st G is configuration & {a1,a2} on A & {b1,b2} on B & a1,a2 |' B & b1,b2 |' A & a1 <> a2 & b1 <> b2 holds a1,a2,b1,b2 is_a_quadrangle let A, B be LINE of G; ::_thesis: ( G is configuration & {a1,a2} on A & {b1,b2} on B & a1,a2 |' B & b1,b2 |' A & a1 <> a2 & b1 <> b2 implies a1,a2,b1,b2 is_a_quadrangle ) assume that A1: G is configuration and A2: {a1,a2} on A and A3: {b1,b2} on B and A4: a1,a2 |' B and A5: b1,b2 |' A and A6: a1 <> a2 and A7: b1 <> b2 ; ::_thesis: a1,a2,b1,b2 is_a_quadrangle b1 |' A by A5, Def1; then A8: a1,a2,b1 is_a_triangle by A1, A2, A6, Th10; b2 |' A by A5, Def1; then a1,a2,b2 is_a_triangle by A1, A2, A6, Th10; then A9: b2,a1,a2 is_a_triangle by Th11; a2 |' B by A4, Def1; then b1,b2,a2 is_a_triangle by A1, A3, A7, Th10; then A10: a2,b1,b2 is_a_triangle by Th11; a1 |' B by A4, Def1; then b1,b2,a1 is_a_triangle by A1, A3, A7, Th10; hence a1,a2,b1,b2 is_a_quadrangle by A8, A10, A9, Def6; ::_thesis: verum end; theorem Th15: :: PROJPL_1:15 for G being IncProjStr st G is IncProjSp holds ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle proof let G be IncProjStr ; ::_thesis: ( G is IncProjSp implies ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle ) assume A1: G is IncProjSp ; ::_thesis: ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle then consider A, B being LINE of G such that A2: A <> B by Th7; consider a, b being POINT of G such that A3: ( a on A & a |' B ) and A4: ( b on B & b |' A ) by A1, A2, PROJRED1:3; consider q being POINT of G such that A5: ( q on B & q |' A ) and A6: b <> q by A1, A3, Th9; A7: ( {b,q} on B & b,q |' A ) by A4, A5, Def1, INCSP_1:1; A8: G is configuration by A1, Th4; consider p being POINT of G such that A9: ( p on A & p |' B ) and A10: a <> p by A1, A3, Th9; take a ; ::_thesis: ex b, c, d being POINT of G st a,b,c,d is_a_quadrangle take p ; ::_thesis: ex c, d being POINT of G st a,p,c,d is_a_quadrangle take b ; ::_thesis: ex d being POINT of G st a,p,b,d is_a_quadrangle take q ; ::_thesis: a,p,b,q is_a_quadrangle ( {a,p} on A & a,p |' B ) by A3, A9, Def1, INCSP_1:1; hence a,p,b,q is_a_quadrangle by A10, A6, A8, A7, Th14; ::_thesis: verum end; definition let G be IncProjSp; mode Quadrangle of G -> Element of [: the Points of G, the Points of G, the Points of G, the Points of G:] means :: PROJPL_1:def 7 it `1_4 ,it `2_4 ,it `3_4 ,it `4_4 is_a_quadrangle ; existence ex b1 being Element of [: the Points of G, the Points of G, the Points of G, the Points of G:] st b1 `1_4 ,b1 `2_4 ,b1 `3_4 ,b1 `4_4 is_a_quadrangle proof consider a, b, c, d being POINT of G such that A1: a,b,c,d is_a_quadrangle by Th15; reconsider e = [a,b,c,d] as Element of [: the Points of G, the Points of G, the Points of G, the Points of G:] ; A2: e `3_4 = c by MCART_1:def_10; take e ; ::_thesis: e `1_4 ,e `2_4 ,e `3_4 ,e `4_4 is_a_quadrangle ( e `1_4 = a & e `2_4 = b ) by MCART_1:def_8, MCART_1:def_9; hence e `1_4 ,e `2_4 ,e `3_4 ,e `4_4 is_a_quadrangle by A1, A2, MCART_1:def_11; ::_thesis: verum end; end; :: deftheorem defines Quadrangle PROJPL_1:def_7_:_ for G being IncProjSp for b2 being Element of [: the Points of G, the Points of G, the Points of G, the Points of G:] holds ( b2 is Quadrangle of G iff b2 `1_4 ,b2 `2_4 ,b2 `3_4 ,b2 `4_4 is_a_quadrangle ); definition let G be IncProjSp; let a, b be POINT of G; assume A1: a <> b ; funca * b -> LINE of G means :Def8: :: PROJPL_1:def 8 {a,b} on it; existence ex b1 being LINE of G st {a,b} on b1 by Th4; uniqueness for b1, b2 being LINE of G st {a,b} on b1 & {a,b} on b2 holds b1 = b2 proof G is configuration by Th4; hence for b1, b2 being LINE of G st {a,b} on b1 & {a,b} on b2 holds b1 = b2 by A1, Th2; ::_thesis: verum end; end; :: deftheorem Def8 defines * PROJPL_1:def_8_:_ for G being IncProjSp for a, b being POINT of G st a <> b holds for b4 being LINE of G holds ( b4 = a * b iff {a,b} on b4 ); theorem Th16: :: PROJPL_1:16 for G being IncProjSp for a, b being POINT of G for L being LINE of G st a <> b holds ( a on a * b & b on a * b & a * b = b * a & ( a on L & b on L implies L = a * b ) ) proof let G be IncProjSp; ::_thesis: for a, b being POINT of G for L being LINE of G st a <> b holds ( a on a * b & b on a * b & a * b = b * a & ( a on L & b on L implies L = a * b ) ) let a, b be POINT of G; ::_thesis: for L being LINE of G st a <> b holds ( a on a * b & b on a * b & a * b = b * a & ( a on L & b on L implies L = a * b ) ) let L be LINE of G; ::_thesis: ( a <> b implies ( a on a * b & b on a * b & a * b = b * a & ( a on L & b on L implies L = a * b ) ) ) assume A1: a <> b ; ::_thesis: ( a on a * b & b on a * b & a * b = b * a & ( a on L & b on L implies L = a * b ) ) then {a,b} on a * b by Def8; hence ( a on a * b & b on a * b & a * b = b * a ) by A1, Def8, INCSP_1:1; ::_thesis: ( a on L & b on L implies L = a * b ) assume ( a on L & b on L ) ; ::_thesis: L = a * b then {a,b} on L by INCSP_1:1; hence L = a * b by A1, Def8; ::_thesis: verum end; begin theorem Th17: :: PROJPL_1:17 for G being IncProjStr st ex a, b, c being POINT of G st a,b,c is_a_triangle & ( for p, q being POINT of G ex M being LINE of G st {p,q} on M ) holds ex p being POINT of G ex P being LINE of G st p |' P proof let G be IncProjStr ; ::_thesis: ( ex a, b, c being POINT of G st a,b,c is_a_triangle & ( for p, q being POINT of G ex M being LINE of G st {p,q} on M ) implies ex p being POINT of G ex P being LINE of G st p |' P ) assume that A1: ex a, b, c being POINT of G st a,b,c is_a_triangle and A2: for p, q being POINT of G ex M being LINE of G st {p,q} on M ; ::_thesis: ex p being POINT of G ex P being LINE of G st p |' P consider a, b, c being POINT of G such that A3: a,b,c is_a_triangle by A1; consider P being LINE of G such that A4: {a,b} on P by A2; take c ; ::_thesis: ex P being LINE of G st c |' P take P ; ::_thesis: c |' P ( a on P & b on P ) by A4, INCSP_1:1; hence c |' P by A3, Th5; ::_thesis: verum end; theorem Th18: :: PROJPL_1:18 for G being IncProjStr st ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle holds ex a, b, c being POINT of G st a,b,c is_a_triangle proof let G be IncProjStr ; ::_thesis: ( ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle implies ex a, b, c being POINT of G st a,b,c is_a_triangle ) given a, b, c, d being POINT of G such that A1: a,b,c,d is_a_quadrangle ; ::_thesis: ex a, b, c being POINT of G st a,b,c is_a_triangle take a ; ::_thesis: ex b, c being POINT of G st a,b,c is_a_triangle take b ; ::_thesis: ex c being POINT of G st a,b,c is_a_triangle take c ; ::_thesis: a,b,c is_a_triangle thus a,b,c is_a_triangle by A1, Def6; ::_thesis: verum end; theorem Th19: :: PROJPL_1:19 for G being IncProjStr for a, b, c being POINT of G for P, Q being LINE of G st a,b,c is_a_triangle & {a,b} on P & {a,c} on Q holds P <> Q proof let G be IncProjStr ; ::_thesis: for a, b, c being POINT of G for P, Q being LINE of G st a,b,c is_a_triangle & {a,b} on P & {a,c} on Q holds P <> Q let a, b, c be POINT of G; ::_thesis: for P, Q being LINE of G st a,b,c is_a_triangle & {a,b} on P & {a,c} on Q holds P <> Q let P, Q be LINE of G; ::_thesis: ( a,b,c is_a_triangle & {a,b} on P & {a,c} on Q implies P <> Q ) assume that A1: a,b,c is_a_triangle and A2: {a,b} on P and A3: {a,c} on Q ; ::_thesis: P <> Q A4: c on Q by A3, INCSP_1:1; ( a on P & b on P ) by A2, INCSP_1:1; hence P <> Q by A1, A4, Th5; ::_thesis: verum end; theorem Th20: :: PROJPL_1:20 for G being IncProjStr for a, b, c, d being POINT of G for P, Q, R being LINE of G st a,b,c,d is_a_quadrangle & {a,b} on P & {a,c} on Q & {a,d} on R holds P,Q,R are_mutually_different proof let G be IncProjStr ; ::_thesis: for a, b, c, d being POINT of G for P, Q, R being LINE of G st a,b,c,d is_a_quadrangle & {a,b} on P & {a,c} on Q & {a,d} on R holds P,Q,R are_mutually_different let a, b, c, d be POINT of G; ::_thesis: for P, Q, R being LINE of G st a,b,c,d is_a_quadrangle & {a,b} on P & {a,c} on Q & {a,d} on R holds P,Q,R are_mutually_different let P, Q, R be LINE of G; ::_thesis: ( a,b,c,d is_a_quadrangle & {a,b} on P & {a,c} on Q & {a,d} on R implies P,Q,R are_mutually_different ) assume that A1: a,b,c,d is_a_quadrangle and A2: {a,b} on P and A3: {a,c} on Q and A4: {a,d} on R ; ::_thesis: P,Q,R are_mutually_different c,d,a is_a_triangle by A1, Def6; then a,c,d is_a_triangle by Th11; then A5: Q <> R by A3, A4, Th19; d,a,b is_a_triangle by A1, Def6; then a,d,b is_a_triangle by Th11; then A6: R <> P by A2, A4, Th19; a,b,c is_a_triangle by A1, Def6; then P <> Q by A2, A3, Th19; hence P,Q,R are_mutually_different by A5, A6, ZFMISC_1:def_5; ::_thesis: verum end; theorem Th21: :: PROJPL_1:21 for G being IncProjStr for a, p, q, r being POINT of G for P, Q, R, A being LINE of G st G is configuration & a on P,Q,R & P,Q,R are_mutually_different & a |' A & p on A,P & q on A,Q & r on A,R holds p,q,r are_mutually_different proof let G be IncProjStr ; ::_thesis: for a, p, q, r being POINT of G for P, Q, R, A being LINE of G st G is configuration & a on P,Q,R & P,Q,R are_mutually_different & a |' A & p on A,P & q on A,Q & r on A,R holds p,q,r are_mutually_different let a, p, q, r be POINT of G; ::_thesis: for P, Q, R, A being LINE of G st G is configuration & a on P,Q,R & P,Q,R are_mutually_different & a |' A & p on A,P & q on A,Q & r on A,R holds p,q,r are_mutually_different let P, Q, R, A be LINE of G; ::_thesis: ( G is configuration & a on P,Q,R & P,Q,R are_mutually_different & a |' A & p on A,P & q on A,Q & r on A,R implies p,q,r are_mutually_different ) assume that A1: G is configuration and A2: a on P,Q,R and A3: P,Q,R are_mutually_different and A4: a |' A and A5: p on A,P and A6: q on A,Q and A7: r on A,R ; ::_thesis: p,q,r are_mutually_different A8: ( a on R & r on R ) by A2, A7, Def2, Def3; A9: ( a on Q & q on Q ) by A2, A6, Def2, Def3; ( Q <> R & q on A ) by A3, A6, Def2, ZFMISC_1:def_5; then A10: q <> r by A1, A4, A9, A8, Def4; A11: p on P by A5, Def2; A12: ( a on P & p on A ) by A2, A5, Def2, Def3; R <> P by A3, ZFMISC_1:def_5; then A13: r <> p by A1, A4, A12, A11, A8, Def4; P <> Q by A3, ZFMISC_1:def_5; then p <> q by A1, A4, A12, A11, A9, Def4; hence p,q,r are_mutually_different by A10, A13, ZFMISC_1:def_5; ::_thesis: verum end; theorem Th22: :: PROJPL_1:22 for G being IncProjStr st G is configuration & ( for p, q being POINT of G ex M being LINE of G st {p,q} on M ) & ( for P, Q being LINE of G ex a being POINT of G st a on P,Q ) & ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle holds for P being LINE of G ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) proof let G be IncProjStr ; ::_thesis: ( G is configuration & ( for p, q being POINT of G ex M being LINE of G st {p,q} on M ) & ( for P, Q being LINE of G ex a being POINT of G st a on P,Q ) & ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle implies for P being LINE of G ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) ) assume that A1: G is configuration and A2: for p, q being POINT of G ex M being LINE of G st {p,q} on M and A3: for P, Q being LINE of G ex a being POINT of G st a on P,Q and A4: ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle ; ::_thesis: for P being LINE of G ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) hereby ::_thesis: verum let P be LINE of G; ::_thesis: ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) consider a, b, c, d being POINT of G such that A5: a,b,c,d is_a_quadrangle by A4; A6: a,b,c is_a_triangle by A5, Def6; thus ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) ::_thesis: verum proof now__::_thesis:_(_(_a_|'_P_&_ex_a,_b,_c_being_POINT_of_G_st_ (_a,b,c_are_mutually_different_&_{a,b,c}_on_P_)_)_or_(_b_|'_P_&_ex_a,_b,_c_being_POINT_of_G_st_ (_a,b,c_are_mutually_different_&_{a,b,c}_on_P_)_)_or_(_c_|'_P_&_ex_a,_b,_c_being_POINT_of_G_st_ (_a,b,c_are_mutually_different_&_{a,b,c}_on_P_)_)_) percases ( a |' P or b |' P or c |' P ) by A6, Th5; caseA7: a |' P ; ::_thesis: ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) consider B being LINE of G such that A8: {a,b} on B by A2; consider D being LINE of G such that A9: {a,d} on D by A2; consider C being LINE of G such that A10: {a,c} on C by A2; A11: a on D by A9, INCSP_1:1; A12: a on C by A10, INCSP_1:1; a on B by A8, INCSP_1:1; then A13: a on B,C,D by A12, A11, Def3; consider p being POINT of G such that A14: p on P,B by A3; A15: B,C,D are_mutually_different by A5, A8, A10, A9, Th20; consider q being POINT of G such that A16: q on P,C by A3; A17: q on P by A16, Def2; consider r being POINT of G such that A18: r on P,D by A3; A19: r on P by A18, Def2; p on P by A14, Def2; then {p,q,r} on P by A17, A19, INCSP_1:2; hence ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) by A1, A7, A13, A15, A14, A16, A18, Th21; ::_thesis: verum end; caseA20: b |' P ; ::_thesis: ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) consider B being LINE of G such that A21: {b,a} on B by A2; consider D being LINE of G such that A22: {b,d} on D by A2; consider C being LINE of G such that A23: {b,c} on C by A2; A24: b on D by A22, INCSP_1:1; A25: b on C by A23, INCSP_1:1; b on B by A21, INCSP_1:1; then A26: b on B,C,D by A25, A24, Def3; consider q being POINT of G such that A27: q on P,C by A3; b,a,c,d is_a_quadrangle by A5, Th13; then A28: B,C,D are_mutually_different by A21, A23, A22, Th20; consider p being POINT of G such that A29: p on P,B by A3; A30: q on P by A27, Def2; consider r being POINT of G such that A31: r on P,D by A3; A32: r on P by A31, Def2; p on P by A29, Def2; then {p,q,r} on P by A30, A32, INCSP_1:2; hence ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) by A1, A20, A26, A28, A29, A27, A31, Th21; ::_thesis: verum end; caseA33: c |' P ; ::_thesis: ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) consider B being LINE of G such that A34: {c,a} on B by A2; consider D being LINE of G such that A35: {c,d} on D by A2; consider C being LINE of G such that A36: {c,b} on C by A2; A37: c on D by A35, INCSP_1:1; A38: c on C by A36, INCSP_1:1; c on B by A34, INCSP_1:1; then A39: c on B,C,D by A38, A37, Def3; consider q being POINT of G such that A40: q on P,C by A3; c,a,b,d is_a_quadrangle by A5, Th13; then A41: B,C,D are_mutually_different by A34, A36, A35, Th20; consider p being POINT of G such that A42: p on P,B by A3; A43: q on P by A40, Def2; consider r being POINT of G such that A44: r on P,D by A3; A45: r on P by A44, Def2; p on P by A42, Def2; then {p,q,r} on P by A43, A45, INCSP_1:2; hence ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) by A1, A33, A39, A41, A42, A40, A44, Th21; ::_thesis: verum end; end; end; hence ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) ; ::_thesis: verum end; end; end; theorem Th23: :: PROJPL_1:23 for G being IncProjStr holds ( G is IncProjectivePlane iff ( G is configuration & ( for p, q being POINT of G ex M being LINE of G st {p,q} on M ) & ( for P, Q being LINE of G ex a being POINT of G st a on P,Q ) & ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle ) ) proof let G be IncProjStr ; ::_thesis: ( G is IncProjectivePlane iff ( G is configuration & ( for p, q being POINT of G ex M being LINE of G st {p,q} on M ) & ( for P, Q being LINE of G ex a being POINT of G st a on P,Q ) & ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle ) ) hereby ::_thesis: ( G is configuration & ( for p, q being POINT of G ex M being LINE of G st {p,q} on M ) & ( for P, Q being LINE of G ex a being POINT of G st a on P,Q ) & ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle implies G is IncProjectivePlane ) assume A1: G is IncProjectivePlane ; ::_thesis: ( G is configuration & ( for p, q being POINT of G ex M being LINE of G st {p,q} on M ) & ( for P, Q being LINE of G ex a being POINT of G st a on P,Q ) & ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle ) hence G is configuration by Th4; ::_thesis: ( ( for p, q being POINT of G ex M being LINE of G st {p,q} on M ) & ( for P, Q being LINE of G ex a being POINT of G st a on P,Q ) & ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle ) thus for p, q being POINT of G ex M being LINE of G st {p,q} on M by A1, Th4; ::_thesis: ( ( for P, Q being LINE of G ex a being POINT of G st a on P,Q ) & ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle ) thus for P, Q being LINE of G ex a being POINT of G st a on P,Q ::_thesis: ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle proof let P, Q be LINE of G; ::_thesis: ex a being POINT of G st a on P,Q consider a being POINT of G such that A2: ( a on P & a on Q ) by A1, INCPROJ:def_9; take a ; ::_thesis: a on P,Q thus a on P,Q by A2, Def2; ::_thesis: verum end; thus ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle by A1, Th15; ::_thesis: verum end; hereby ::_thesis: verum assume that A3: G is configuration and A4: for p, q being POINT of G ex M being LINE of G st {p,q} on M and A5: for P, Q being LINE of G ex a being POINT of G st a on P,Q and A6: ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle ; ::_thesis: G is IncProjectivePlane ex a, b, c being POINT of G st a,b,c is_a_triangle by A6, Th18; then A7: ex p being POINT of G ex P being LINE of G st p |' P by A4, Th17; ( ( for P being LINE of G ex a, b, c being POINT of G st ( a,b,c are_mutually_different & {a,b,c} on P ) ) & ( for a, b, c, d, p being POINT of G for M, N, P, Q being LINE of G st {a,b,p} on M & {c,d,p} on N & {a,c} on P & {b,d} on Q & p |' P & p |' Q & M <> N holds ex q being POINT of G st q on P,Q ) ) by A3, A4, A5, A6, Th22; then reconsider G9 = G as IncProjSp by A3, A4, A7, Th4; for P, Q being LINE of G9 ex a being POINT of G9 st ( a on P & a on Q ) proof let P, Q be LINE of G9; ::_thesis: ex a being POINT of G9 st ( a on P & a on Q ) consider a being POINT of G9 such that A8: a on P,Q by A5; take a ; ::_thesis: ( a on P & a on Q ) thus ( a on P & a on Q ) by A8, Def2; ::_thesis: verum end; hence G is IncProjectivePlane by INCPROJ:def_9; ::_thesis: verum end; end; definition let G be IncProjectivePlane; let A, B be LINE of G; assume A1: A <> B ; funcA * B -> POINT of G means :Def9: :: PROJPL_1:def 9 it on A,B; existence ex b1 being POINT of G st b1 on A,B by Th23; uniqueness for b1, b2 being POINT of G st b1 on A,B & b2 on A,B holds b1 = b2 proof G is configuration by Th4; hence for b1, b2 being POINT of G st b1 on A,B & b2 on A,B holds b1 = b2 by A1, Th3; ::_thesis: verum end; end; :: deftheorem Def9 defines * PROJPL_1:def_9_:_ for G being IncProjectivePlane for A, B being LINE of G st A <> B holds for b4 being POINT of G holds ( b4 = A * B iff b4 on A,B ); theorem Th24: :: PROJPL_1:24 for G being IncProjectivePlane for a being POINT of G for A, B being LINE of G st A <> B holds ( A * B on A & A * B on B & A * B = B * A & ( a on A & a on B implies a = A * B ) ) proof let G be IncProjectivePlane; ::_thesis: for a being POINT of G for A, B being LINE of G st A <> B holds ( A * B on A & A * B on B & A * B = B * A & ( a on A & a on B implies a = A * B ) ) let a be POINT of G; ::_thesis: for A, B being LINE of G st A <> B holds ( A * B on A & A * B on B & A * B = B * A & ( a on A & a on B implies a = A * B ) ) let A, B be LINE of G; ::_thesis: ( A <> B implies ( A * B on A & A * B on B & A * B = B * A & ( a on A & a on B implies a = A * B ) ) ) assume A1: A <> B ; ::_thesis: ( A * B on A & A * B on B & A * B = B * A & ( a on A & a on B implies a = A * B ) ) then A * B on A,B by Def9; then A * B on B,A by Th1; hence ( A * B on A & A * B on B & A * B = B * A ) by A1, Def2, Def9; ::_thesis: ( a on A & a on B implies a = A * B ) assume ( a on A & a on B ) ; ::_thesis: a = A * B then a on A,B by Def2; hence a = A * B by A1, Def9; ::_thesis: verum end; theorem :: PROJPL_1:25 for G being IncProjectivePlane for a, q being POINT of G for A, B being LINE of G st A <> B & a on A & q |' A & a <> A * B holds ( (q * a) * B on B & (q * a) * B |' A ) proof let G be IncProjectivePlane; ::_thesis: for a, q being POINT of G for A, B being LINE of G st A <> B & a on A & q |' A & a <> A * B holds ( (q * a) * B on B & (q * a) * B |' A ) let a, q be POINT of G; ::_thesis: for A, B being LINE of G st A <> B & a on A & q |' A & a <> A * B holds ( (q * a) * B on B & (q * a) * B |' A ) let A, B be LINE of G; ::_thesis: ( A <> B & a on A & q |' A & a <> A * B implies ( (q * a) * B on B & (q * a) * B |' A ) ) assume that A1: A <> B and A2: a on A and A3: q |' A and A4: a <> A * B ; ::_thesis: ( (q * a) * B on B & (q * a) * B |' A ) set D = q * a; A5: ( a on q * a & q on q * a ) by A2, A3, Th16; set d = (q * a) * B; A6: G is configuration by Th23; A7: a |' B by A1, A2, A4, Th24; then A8: q * a <> B by A2, A3, Th16; hence (q * a) * B on B by Th24; ::_thesis: (q * a) * B |' A assume A9: (q * a) * B on A ; ::_thesis: contradiction (q * a) * B on q * a by A8, Th24; then a = (q * a) * B by A2, A3, A6, A9, A5, Def4; hence contradiction by A7, A8, Th24; ::_thesis: verum end; begin theorem Th26: :: PROJPL_1:26 for G being IncProjSp for a, b, c being POINT of G st a,b,c is_a_triangle holds a,b,c are_mutually_different proof let G be IncProjSp; ::_thesis: for a, b, c being POINT of G st a,b,c is_a_triangle holds a,b,c are_mutually_different let a, b, c be POINT of G; ::_thesis: ( a,b,c is_a_triangle implies a,b,c are_mutually_different ) assume that A1: a,b,c is_a_triangle and A2: not a,b,c are_mutually_different ; ::_thesis: contradiction now__::_thesis:_(_(_a_=_b_&_contradiction_)_or_(_b_=_c_&_contradiction_)_or_(_c_=_a_&_contradiction_)_) percases ( a = b or b = c or c = a ) by A2, ZFMISC_1:def_5; caseA3: a = b ; ::_thesis: contradiction ex P being LINE of G st ( b on P & c on P ) by INCPROJ:def_5; hence contradiction by A1, A3, Th5; ::_thesis: verum end; caseA4: b = c ; ::_thesis: contradiction ex P being LINE of G st ( a on P & b on P ) by INCPROJ:def_5; hence contradiction by A1, A4, Th5; ::_thesis: verum end; caseA5: c = a ; ::_thesis: contradiction ex P being LINE of G st ( b on P & c on P ) by INCPROJ:def_5; hence contradiction by A1, A5, Th5; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; theorem :: PROJPL_1:27 for G being IncProjSp for a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle holds a,b,c,d are_mutually_different proof let G be IncProjSp; ::_thesis: for a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle holds a,b,c,d are_mutually_different let a, b, c, d be POINT of G; ::_thesis: ( a,b,c,d is_a_quadrangle implies a,b,c,d are_mutually_different ) assume that A1: a,b,c,d is_a_quadrangle and A2: not a,b,c,d are_mutually_different ; ::_thesis: contradiction now__::_thesis:_(_(_a_=_b_&_contradiction_)_or_(_b_=_c_&_contradiction_)_or_(_c_=_a_&_contradiction_)_or_(_d_=_a_&_contradiction_)_or_(_d_=_b_&_contradiction_)_or_(_d_=_c_&_contradiction_)_) percases ( a = b or b = c or c = a or d = a or d = b or d = c ) by A2, ZFMISC_1:def_6; case a = b ; ::_thesis: contradiction then not a,b,c are_mutually_different by ZFMISC_1:def_5; then not a,b,c is_a_triangle by Th26; hence contradiction by A1, Def6; ::_thesis: verum end; case b = c ; ::_thesis: contradiction then not a,b,c are_mutually_different by ZFMISC_1:def_5; then not a,b,c is_a_triangle by Th26; hence contradiction by A1, Def6; ::_thesis: verum end; case c = a ; ::_thesis: contradiction then not a,b,c are_mutually_different by ZFMISC_1:def_5; then not a,b,c is_a_triangle by Th26; hence contradiction by A1, Def6; ::_thesis: verum end; case d = a ; ::_thesis: contradiction then not d,a,b are_mutually_different by ZFMISC_1:def_5; then not d,a,b is_a_triangle by Th26; hence contradiction by A1, Def6; ::_thesis: verum end; case d = b ; ::_thesis: contradiction then not d,a,b are_mutually_different by ZFMISC_1:def_5; then not d,a,b is_a_triangle by Th26; hence contradiction by A1, Def6; ::_thesis: verum end; case d = c ; ::_thesis: contradiction then not b,c,d are_mutually_different by ZFMISC_1:def_5; then not b,c,d is_a_triangle by Th26; hence contradiction by A1, Def6; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; theorem Th28: :: PROJPL_1:28 for G being IncProjectivePlane for a, b, c, d being POINT of G holds ( not a * c = b * d or a = c or b = d or c = d or a * c = c * d ) proof let G be IncProjectivePlane; ::_thesis: for a, b, c, d being POINT of G holds ( not a * c = b * d or a = c or b = d or c = d or a * c = c * d ) let a, b, c, d be POINT of G; ::_thesis: ( not a * c = b * d or a = c or b = d or c = d or a * c = c * d ) assume that A1: ( a * c = b * d & not a = c & not b = d ) and A2: not c = d ; ::_thesis: a * c = c * d ( c on a * c & d on a * c ) by A1, Th16; hence a * c = c * d by A2, Th16; ::_thesis: verum end; theorem :: PROJPL_1:29 for G being IncProjectivePlane for a, b, c, d being POINT of G holds ( not a * c = b * d or a = c or b = d or c = d or a on c * d ) proof let G be IncProjectivePlane; ::_thesis: for a, b, c, d being POINT of G holds ( not a * c = b * d or a = c or b = d or c = d or a on c * d ) let a, b, c, d be POINT of G; ::_thesis: ( not a * c = b * d or a = c or b = d or c = d or a on c * d ) assume that A1: a * c = b * d and A2: not a = c and A3: ( not b = d & not c = d ) ; ::_thesis: a on c * d a * c = c * d by A1, A2, A3, Th28; hence a on c * d by A2, Th16; ::_thesis: verum end; theorem :: PROJPL_1:30 for G being IncProjectivePlane for e, m, m9 being POINT of G for I being LINE of G st m on I & m9 on I & m <> m9 & e |' I holds ( m * e <> m9 * e & e * m <> e * m9 ) proof let G be IncProjectivePlane; ::_thesis: for e, m, m9 being POINT of G for I being LINE of G st m on I & m9 on I & m <> m9 & e |' I holds ( m * e <> m9 * e & e * m <> e * m9 ) let e, m, m9 be POINT of G; ::_thesis: for I being LINE of G st m on I & m9 on I & m <> m9 & e |' I holds ( m * e <> m9 * e & e * m <> e * m9 ) let I be LINE of G; ::_thesis: ( m on I & m9 on I & m <> m9 & e |' I implies ( m * e <> m9 * e & e * m <> e * m9 ) ) assume that A1: m on I and A2: m9 on I and A3: m <> m9 and A4: e |' I ; ::_thesis: ( m * e <> m9 * e & e * m <> e * m9 ) set L1 = m * e; set L2 = m9 * e; A5: now__::_thesis:_not_m_*_e_=_m9_*_e m on m * e by A1, A4, Th16; then A6: m on I,m * e by A1, Def2; e on m * e by A1, A4, Th16; then A7: m = I * (m * e) by A4, A6, Def9; assume A8: m * e = m9 * e ; ::_thesis: contradiction m9 on m9 * e by A2, A4, Th16; then A9: m9 on I,m9 * e by A2, Def2; e on m9 * e by A2, A4, Th16; hence contradiction by A3, A4, A8, A9, A7, Def9; ::_thesis: verum end; now__::_thesis:_not_e_*_m_=_e_*_m9 assume A10: e * m = e * m9 ; ::_thesis: contradiction m * e = e * m by A1, A4, Th16; hence contradiction by A2, A4, A5, A10, Th16; ::_thesis: verum end; hence ( m * e <> m9 * e & e * m <> e * m9 ) by A5; ::_thesis: verum end; theorem :: PROJPL_1:31 for G being IncProjectivePlane for e being POINT of G for I, L1, L2 being LINE of G st e on L1 & e on L2 & L1 <> L2 & e |' I holds ( I * L1 <> I * L2 & L1 * I <> L2 * I ) proof let G be IncProjectivePlane; ::_thesis: for e being POINT of G for I, L1, L2 being LINE of G st e on L1 & e on L2 & L1 <> L2 & e |' I holds ( I * L1 <> I * L2 & L1 * I <> L2 * I ) let e be POINT of G; ::_thesis: for I, L1, L2 being LINE of G st e on L1 & e on L2 & L1 <> L2 & e |' I holds ( I * L1 <> I * L2 & L1 * I <> L2 * I ) let I, L1, L2 be LINE of G; ::_thesis: ( e on L1 & e on L2 & L1 <> L2 & e |' I implies ( I * L1 <> I * L2 & L1 * I <> L2 * I ) ) assume that A1: e on L1 and A2: e on L2 and A3: L1 <> L2 and A4: e |' I ; ::_thesis: ( I * L1 <> I * L2 & L1 * I <> L2 * I ) set p1 = I * L1; set p2 = I * L2; A5: now__::_thesis:_not_I_*_L1_=_I_*_L2 I * L1 on L1 by A1, A4, Th24; then A6: {e,(I * L1)} on L1 by A1, INCSP_1:1; I * L1 on I by A1, A4, Th24; then A7: L1 = e * (I * L1) by A4, A6, Def8; assume A8: I * L1 = I * L2 ; ::_thesis: contradiction I * L2 on L2 by A2, A4, Th24; then A9: {e,(I * L2)} on L2 by A2, INCSP_1:1; I * L2 on I by A2, A4, Th24; hence contradiction by A3, A4, A8, A9, A7, Def8; ::_thesis: verum end; now__::_thesis:_not_L1_*_I_=_L2_*_I assume A10: L1 * I = L2 * I ; ::_thesis: contradiction L1 * I = I * L1 by A1, A4, Th24; hence contradiction by A2, A4, A5, A10, Th24; ::_thesis: verum end; hence ( I * L1 <> I * L2 & L1 * I <> L2 * I ) by A5; ::_thesis: verum end; theorem :: PROJPL_1:32 for G being IncProjSp for a, b, q, q1 being POINT of G st q on a * b & q on a * q1 & q <> a & q1 <> a & a <> b holds q1 on a * b proof let G be IncProjSp; ::_thesis: for a, b, q, q1 being POINT of G st q on a * b & q on a * q1 & q <> a & q1 <> a & a <> b holds q1 on a * b let a, b, q, q1 be POINT of G; ::_thesis: ( q on a * b & q on a * q1 & q <> a & q1 <> a & a <> b implies q1 on a * b ) assume that A1: ( q on a * b & q on a * q1 & q <> a ) and A2: q1 <> a and A3: a <> b ; ::_thesis: q1 on a * b ( a on a * b & a on a * q1 ) by A2, A3, Th16; then a * b = a * q1 by A1, INCPROJ:def_4; hence q1 on a * b by A2, Th16; ::_thesis: verum end; theorem :: PROJPL_1:33 for G being IncProjSp for a, b, c being POINT of G st c on a * b & a <> c holds b on a * c proof let G be IncProjSp; ::_thesis: for a, b, c being POINT of G st c on a * b & a <> c holds b on a * c let a, b, c be POINT of G; ::_thesis: ( c on a * b & a <> c implies b on a * c ) assume that A1: c on a * b and A2: a <> c ; ::_thesis: b on a * c now__::_thesis:_(_a_<>_b_implies_b_on_a_*_c_) assume A3: a <> b ; ::_thesis: b on a * c then a on a * b by Th16; then a * b = a * c by A1, A2, Th16; hence b on a * c by A3, Th16; ::_thesis: verum end; hence b on a * c by A2, Th16; ::_thesis: verum end; theorem :: PROJPL_1:34 for G being IncProjectivePlane for q1, q2, r1, r2 being POINT of G for H being LINE of G st r1 <> r2 & r1 on H & r2 on H & q1 |' H & q2 |' H holds q1 * r1 <> q2 * r2 proof let G be IncProjectivePlane; ::_thesis: for q1, q2, r1, r2 being POINT of G for H being LINE of G st r1 <> r2 & r1 on H & r2 on H & q1 |' H & q2 |' H holds q1 * r1 <> q2 * r2 let q1, q2, r1, r2 be POINT of G; ::_thesis: for H being LINE of G st r1 <> r2 & r1 on H & r2 on H & q1 |' H & q2 |' H holds q1 * r1 <> q2 * r2 let H be LINE of G; ::_thesis: ( r1 <> r2 & r1 on H & r2 on H & q1 |' H & q2 |' H implies q1 * r1 <> q2 * r2 ) assume that A1: r1 <> r2 and A2: r1 on H and A3: r2 on H and A4: q1 |' H and A5: q2 |' H and A6: q1 * r1 = q2 * r2 ; ::_thesis: contradiction set L1 = q1 * r1; set L2 = q2 * r2; A7: q1 on q1 * r1 by A2, A4, Th16; r2 on q2 * r2 by A3, A5, Th16; then A8: r2 on q2 * r2,H by A3, Def2; r1 on q1 * r1 by A2, A4, Th16; then r1 on q1 * r1,H by A2, Def2; then r1 = (q1 * r1) * H by A4, A7, Def9; hence contradiction by A1, A4, A6, A7, A8, Def9; ::_thesis: verum end; theorem Th35: :: PROJPL_1:35 for G being IncProjectivePlane for a, b, c being POINT of G holds ( not a on b * c or a = c or b = c or b on c * a ) proof let G be IncProjectivePlane; ::_thesis: for a, b, c being POINT of G holds ( not a on b * c or a = c or b = c or b on c * a ) let a, b, c be POINT of G; ::_thesis: ( not a on b * c or a = c or b = c or b on c * a ) assume that A1: a on b * c and A2: a <> c and A3: b <> c ; ::_thesis: b on c * a c on b * c by A3, Th16; then A4: {c,a} on b * c by A1, INCSP_1:1; b on b * c by A3, Th16; hence b on c * a by A2, A4, Def8; ::_thesis: verum end; theorem :: PROJPL_1:36 for G being IncProjectivePlane for a, b, c being POINT of G holds ( not a on b * c or b = a or b = c or c on b * a ) proof let G be IncProjectivePlane; ::_thesis: for a, b, c being POINT of G holds ( not a on b * c or b = a or b = c or c on b * a ) let a, b, c be POINT of G; ::_thesis: ( not a on b * c or b = a or b = c or c on b * a ) assume that A1: ( a on b * c & b <> a ) and A2: b <> c ; ::_thesis: c on b * a b * c = c * b by A2, Th16; hence c on b * a by A1, A2, Th35; ::_thesis: verum end; theorem :: PROJPL_1:37 for G being IncProjectivePlane for e, x1, x2, p1, p2 being POINT of G for H, I being LINE of G st x1 on I & x2 on I & e |' I & x1 <> x2 & p1 <> e & p2 <> e & p1 on e * x1 & p2 on e * x2 holds ex r being POINT of G st ( r on p1 * p2 & r on H & r <> e ) proof let G be IncProjectivePlane; ::_thesis: for e, x1, x2, p1, p2 being POINT of G for H, I being LINE of G st x1 on I & x2 on I & e |' I & x1 <> x2 & p1 <> e & p2 <> e & p1 on e * x1 & p2 on e * x2 holds ex r being POINT of G st ( r on p1 * p2 & r on H & r <> e ) let e, x1, x2, p1, p2 be POINT of G; ::_thesis: for H, I being LINE of G st x1 on I & x2 on I & e |' I & x1 <> x2 & p1 <> e & p2 <> e & p1 on e * x1 & p2 on e * x2 holds ex r being POINT of G st ( r on p1 * p2 & r on H & r <> e ) let H, I be LINE of G; ::_thesis: ( x1 on I & x2 on I & e |' I & x1 <> x2 & p1 <> e & p2 <> e & p1 on e * x1 & p2 on e * x2 implies ex r being POINT of G st ( r on p1 * p2 & r on H & r <> e ) ) assume that A1: x1 on I and A2: x2 on I and A3: e |' I and A4: x1 <> x2 and A5: p1 <> e and A6: p2 <> e and A7: p1 on e * x1 and A8: p2 on e * x2 ; ::_thesis: ex r being POINT of G st ( r on p1 * p2 & r on H & r <> e ) set L1 = e * x1; set L2 = e * x2; set L = p1 * p2; A9: e on e * x1 by A1, A3, Th16; A10: e on e * x2 by A2, A3, Th16; ( x1 on e * x1 & x2 on e * x2 ) by A1, A2, A3, Th16; then A11: e * x1 <> e * x2 by A1, A2, A3, A4, A9, INCPROJ:def_4; then A12: p1 <> p2 by A5, A7, A8, A9, A10, INCPROJ:def_4; then p2 on p1 * p2 by Th16; then A13: p1 * p2 <> e * x1 by A6, A8, A9, A10, A11, INCPROJ:def_4; consider r being POINT of G such that A14: r on p1 * p2 and A15: r on H by INCPROJ:def_9; p1 on p1 * p2 by A12, Th16; then r <> e by A5, A7, A14, A9, A13, INCPROJ:def_4; hence ex r being POINT of G st ( r on p1 * p2 & r on H & r <> e ) by A14, A15; ::_thesis: verum end;