:: PROJRED1 semantic presentation begin theorem Th1: :: PROJRED1:1 for IPP being IncProjSp for A being LINE of IPP holds not for a being POINT of IPP holds a on A proof let IPP be IncProjSp; ::_thesis: for A being LINE of IPP holds not for a being POINT of IPP holds a on A let A be LINE of IPP; ::_thesis: not for a being POINT of IPP holds a on A consider p being POINT of IPP, L being LINE of IPP such that A1: not p on L by INCPROJ:def_6; now__::_thesis:_(_A_<>_L_implies_ex_a_being_POINT_of_IPP_st_not_a_on_A_) assume A2: A <> L ; ::_thesis: not for a being POINT of IPP holds a on A now__::_thesis:_not_for_a_being_POINT_of_IPP_holds_a_on_A consider q, r, s being POINT of IPP such that A3: q <> r and r <> s and s <> q and A4: ( q on L & r on L ) and s on L by INCPROJ:def_7; ( not q on A or not r on A ) by A2, A3, A4, INCPROJ:def_4; hence not for a being POINT of IPP holds a on A ; ::_thesis: verum end; hence not for a being POINT of IPP holds a on A ; ::_thesis: verum end; hence not for a being POINT of IPP holds a on A by A1; ::_thesis: verum end; theorem Th2: :: PROJRED1:2 for IPP being IncProjSp for a being POINT of IPP holds not for A being LINE of IPP holds a on A proof let IPP be IncProjSp; ::_thesis: for a being POINT of IPP holds not for A being LINE of IPP holds a on A let a be POINT of IPP; ::_thesis: not for A being LINE of IPP holds a on A consider p being POINT of IPP, L being LINE of IPP such that A1: not p on L by INCPROJ:def_6; now__::_thesis:_not_for_A_being_LINE_of_IPP_holds_a_on_A now__::_thesis:_(_a_on_L_implies_ex_A_being_LINE_of_IPP_st_not_a_on_A_) consider q, r, s being POINT of IPP such that q <> r and r <> s and A2: s <> q and A3: q on L and r on L and A4: s on L by INCPROJ:def_7; assume A5: a on L ; ::_thesis: not for A being LINE of IPP holds a on A A6: now__::_thesis:_(_a_<>_s_implies_ex_A_being_LINE_of_IPP_st_not_a_on_A_) consider S being LINE of IPP such that A7: ( s on S & p on S ) by INCPROJ:def_5; assume a <> s ; ::_thesis: not for A being LINE of IPP holds a on A then not a on S by A1, A5, A4, A7, INCPROJ:def_4; hence not for A being LINE of IPP holds a on A ; ::_thesis: verum end; now__::_thesis:_(_a_<>_q_implies_ex_A_being_LINE_of_IPP_st_not_a_on_A_) consider S being LINE of IPP such that A8: ( q on S & p on S ) by INCPROJ:def_5; assume a <> q ; ::_thesis: not for A being LINE of IPP holds a on A then not a on S by A1, A5, A3, A8, INCPROJ:def_4; hence not for A being LINE of IPP holds a on A ; ::_thesis: verum end; hence not for A being LINE of IPP holds a on A by A2, A6; ::_thesis: verum end; hence not for A being LINE of IPP holds a on A ; ::_thesis: verum end; hence not for A being LINE of IPP holds a on A ; ::_thesis: verum end; theorem Th3: :: PROJRED1:3 for IPP being IncProjSp for A, B being LINE of IPP st A <> B holds ex a, b being POINT of IPP st ( a on A & not a on B & b on B & not b on A ) proof let IPP be IncProjSp; ::_thesis: for A, B being LINE of IPP st A <> B holds ex a, b being POINT of IPP st ( a on A & not a on B & b on B & not b on A ) let A, B be LINE of IPP; ::_thesis: ( A <> B implies ex a, b being POINT of IPP st ( a on A & not a on B & b on B & not b on A ) ) consider a, b, d being POINT of IPP such that A1: a <> b and b <> d and d <> a and A2: ( a on A & b on A ) and d on A by INCPROJ:def_7; consider r, s, t being POINT of IPP such that A3: r <> s and s <> t and t <> r and A4: ( r on B & s on B ) and t on B by INCPROJ:def_7; assume A5: A <> B ; ::_thesis: ex a, b being POINT of IPP st ( a on A & not a on B & b on B & not b on A ) then A6: ( not r on A or not s on A ) by A3, A4, INCPROJ:def_4; ( not a on B or not b on B ) by A5, A1, A2, INCPROJ:def_4; hence ex a, b being POINT of IPP st ( a on A & not a on B & b on B & not b on A ) by A2, A4, A6; ::_thesis: verum end; theorem :: PROJRED1:4 for IPP being IncProjSp for a, b being POINT of IPP st a <> b holds ex A, B being LINE of IPP st ( a on A & not a on B & b on B & not b on A ) proof let IPP be IncProjSp; ::_thesis: for a, b being POINT of IPP st a <> b holds ex A, B being LINE of IPP st ( a on A & not a on B & b on B & not b on A ) let a, b be POINT of IPP; ::_thesis: ( a <> b implies ex A, B being LINE of IPP st ( a on A & not a on B & b on B & not b on A ) ) consider Q being LINE of IPP such that A1: ( a on Q & b on Q ) by INCPROJ:def_5; consider q being POINT of IPP such that A2: not q on Q by Th1; consider B being LINE of IPP such that A3: b on B and A4: q on B by INCPROJ:def_5; assume A5: a <> b ; ::_thesis: ex A, B being LINE of IPP st ( a on A & not a on B & b on B & not b on A ) then A6: not a on B by A1, A2, A3, A4, INCPROJ:def_4; consider A being LINE of IPP such that A7: a on A and A8: q on A by INCPROJ:def_5; not b on A by A5, A1, A2, A7, A8, INCPROJ:def_4; hence ex A, B being LINE of IPP st ( a on A & not a on B & b on B & not b on A ) by A7, A3, A6; ::_thesis: verum end; theorem :: PROJRED1:5 for IPP being IncProjSp for a being POINT of IPP ex A, B, C being LINE of IPP st ( a on A & a on B & a on C & A <> B & B <> C & C <> A ) proof let IPP be IncProjSp; ::_thesis: for a being POINT of IPP ex A, B, C being LINE of IPP st ( a on A & a on B & a on C & A <> B & B <> C & C <> A ) let a be POINT of IPP; ::_thesis: ex A, B, C being LINE of IPP st ( a on A & a on B & a on C & A <> B & B <> C & C <> A ) consider Q being LINE of IPP such that A1: not a on Q by Th2; consider b1, b2, b3 being Element of the Points of IPP such that A2: b1 <> b2 and A3: b2 <> b3 and A4: b3 <> b1 and A5: b1 on Q and A6: b2 on Q and A7: b3 on Q by INCPROJ:def_7; consider B1 being LINE of IPP such that A8: ( a on B1 & b1 on B1 ) by INCPROJ:def_5; A9: not b3 on B1 by A1, A4, A5, A7, A8, INCPROJ:def_4; consider B2 being LINE of IPP such that A10: ( a on B2 & b2 on B2 ) by INCPROJ:def_5; consider B3 being Element of the Lines of IPP such that A11: ( a on B3 & b3 on B3 ) by INCPROJ:def_5; A12: not b2 on B3 by A1, A3, A6, A7, A11, INCPROJ:def_4; not b1 on B2 by A1, A2, A5, A6, A10, INCPROJ:def_4; hence ex A, B, C being LINE of IPP st ( a on A & a on B & a on C & A <> B & B <> C & C <> A ) by A8, A10, A11, A12, A9; ::_thesis: verum end; theorem :: PROJRED1:6 for IPP being IncProjSp for A, B being LINE of IPP ex a being POINT of IPP st ( not a on A & not a on B ) proof let IPP be IncProjSp; ::_thesis: for A, B being LINE of IPP ex a being POINT of IPP st ( not a on A & not a on B ) let A, B be LINE of IPP; ::_thesis: ex a being POINT of IPP st ( not a on A & not a on B ) A1: ( A <> B implies ex a being POINT of IPP st ( not a on A & not a on B ) ) proof assume A <> B ; ::_thesis: ex a being POINT of IPP st ( not a on A & not a on B ) then consider a, b being POINT of IPP such that a on A and A2: not a on B and b on B and A3: not b on A by Th3; consider C being LINE of IPP such that A4: ( a on C & b on C ) by INCPROJ:def_5; consider c, d, e being Element of the Points of IPP such that A5: ( c <> d & d <> e & e <> c & c on C & d on C & e on C ) by INCPROJ:def_7; ( ( not c on A & not c on B ) or ( not d on A & not d on B ) or ( not e on A & not e on B ) ) by A2, A3, A4, A5, INCPROJ:def_4; hence ex a being POINT of IPP st ( not a on A & not a on B ) ; ::_thesis: verum end; ( A = B implies ex a being POINT of IPP st ( not a on A & not a on B ) ) proof assume A6: A = B ; ::_thesis: ex a being POINT of IPP st ( not a on A & not a on B ) not for a being POINT of IPP holds a on A by Th1; hence ex a being POINT of IPP st ( not a on A & not a on B ) by A6; ::_thesis: verum end; hence ex a being POINT of IPP st ( not a on A & not a on B ) by A1; ::_thesis: verum end; theorem Th7: :: PROJRED1:7 for IPP being IncProjSp for A being LINE of IPP ex a being POINT of IPP st a on A proof let IPP be IncProjSp; ::_thesis: for A being LINE of IPP ex a being POINT of IPP st a on A let A be LINE of IPP; ::_thesis: ex a being POINT of IPP st a on A consider a, b, c being POINT of IPP such that a <> b and b <> c and c <> a and A1: a on A and b on A and c on A by INCPROJ:def_7; take a ; ::_thesis: a on A thus a on A by A1; ::_thesis: verum end; theorem Th8: :: PROJRED1:8 for IPP being IncProjSp for a, b being POINT of IPP for A being LINE of IPP ex c being POINT of IPP st ( c on A & c <> a & c <> b ) proof let IPP be IncProjSp; ::_thesis: for a, b being POINT of IPP for A being LINE of IPP ex c being POINT of IPP st ( c on A & c <> a & c <> b ) let a, b be POINT of IPP; ::_thesis: for A being LINE of IPP ex c being POINT of IPP st ( c on A & c <> a & c <> b ) let A be LINE of IPP; ::_thesis: ex c being POINT of IPP st ( c on A & c <> a & c <> b ) consider p, q, r being POINT of IPP such that A1: ( p <> q & q <> r & r <> p ) and A2: ( p on A & q on A & r on A ) by INCPROJ:def_7; ( ( p <> a & p <> b ) or ( q <> a & q <> b ) or ( r <> a & r <> b ) ) by A1; hence ex c being POINT of IPP st ( c on A & c <> a & c <> b ) by A2; ::_thesis: verum end; theorem :: PROJRED1:9 for IPP being IncProjSp for a, b being POINT of IPP ex A being LINE of IPP st ( not a on A & not b on A ) proof let IPP be IncProjSp; ::_thesis: for a, b being POINT of IPP ex A being LINE of IPP st ( not a on A & not b on A ) let a, b be POINT of IPP; ::_thesis: ex A being LINE of IPP st ( not a on A & not b on A ) now__::_thesis:_ex_A_being_LINE_of_IPP_st_ (_not_a_on_A_&_not_b_on_A_) consider A being LINE of IPP such that A1: ( a on A & b on A ) by INCPROJ:def_5; consider c being POINT of IPP such that A2: ( c on A & c <> a & c <> b ) by Th8; consider d being POINT of IPP such that A3: not d on A by Th1; consider B being LINE of IPP such that A4: ( d on B & c on B ) by INCPROJ:def_5; ( not a on B & not b on B ) by A1, A2, A3, A4, INCPROJ:def_4; hence ex A being LINE of IPP st ( not a on A & not b on A ) ; ::_thesis: verum end; hence ex A being LINE of IPP st ( not a on A & not b on A ) ; ::_thesis: verum end; theorem Th10: :: PROJRED1:10 for IPP being IncProjSp for o, a, b, c being POINT of IPP for A, B, P, Q being LINE of IPP st o on A & o on B & A <> B & a on A & o <> a & b on B & c on B & b <> c & a on P & b on P & c on Q holds P <> Q proof let IPP be IncProjSp; ::_thesis: for o, a, b, c being POINT of IPP for A, B, P, Q being LINE of IPP st o on A & o on B & A <> B & a on A & o <> a & b on B & c on B & b <> c & a on P & b on P & c on Q holds P <> Q let o, a, b, c be POINT of IPP; ::_thesis: for A, B, P, Q being LINE of IPP st o on A & o on B & A <> B & a on A & o <> a & b on B & c on B & b <> c & a on P & b on P & c on Q holds P <> Q let A, B, P, Q be LINE of IPP; ::_thesis: ( o on A & o on B & A <> B & a on A & o <> a & b on B & c on B & b <> c & a on P & b on P & c on Q implies P <> Q ) assume that A1: ( o on A & o on B & A <> B & a on A & o <> a ) and A2: ( b on B & c on B & b <> c ) and A3: a on P and A4: ( b on P & c on Q ) ; ::_thesis: P <> Q assume not P <> Q ; ::_thesis: contradiction then P = B by A2, A4, INCPROJ:def_4; hence contradiction by A1, A3, INCPROJ:def_4; ::_thesis: verum end; theorem Th11: :: PROJRED1:11 for IPP being IncProjSp for a, b, c being POINT of IPP for A being LINE of IPP st {a,b,c} on A holds ( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A ) proof let IPP be IncProjSp; ::_thesis: for a, b, c being POINT of IPP for A being LINE of IPP st {a,b,c} on A holds ( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A ) let a, b, c be POINT of IPP; ::_thesis: for A being LINE of IPP st {a,b,c} on A holds ( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A ) let A be LINE of IPP; ::_thesis: ( {a,b,c} on A implies ( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A ) ) assume A1: {a,b,c} on A ; ::_thesis: ( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A ) then A2: c on A by INCSP_1:2; ( a on A & b on A ) by A1, INCSP_1:2; hence ( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A ) by A2, INCSP_1:2; ::_thesis: verum end; theorem Th12: :: PROJRED1:12 for IPP being Desarguesian IncProjSp for o, b1, a1, b2, a2, b3, a3, r, s, t being POINT of IPP for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of IPP st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a3 & o <> b1 & o <> b2 & a2 <> b2 holds ex O being LINE of IPP st {r,s,t} on O proof let IPP be Desarguesian IncProjSp; ::_thesis: for o, b1, a1, b2, a2, b3, a3, r, s, t being POINT of IPP for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of IPP st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a3 & o <> b1 & o <> b2 & a2 <> b2 holds ex O being LINE of IPP st {r,s,t} on O let o, b1, a1, b2, a2, b3, a3, r, s, t be POINT of IPP; ::_thesis: for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of IPP st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a3 & o <> b1 & o <> b2 & a2 <> b2 holds ex O being LINE of IPP st {r,s,t} on O let C1, C2, C3, A1, A2, A3, B1, B2, B3 be LINE of IPP; ::_thesis: ( {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a3 & o <> b1 & o <> b2 & a2 <> b2 implies ex O being LINE of IPP st {r,s,t} on O ) assume that A1: {o,b1,a1} on C1 and A2: {o,a2,b2} on C2 and A3: {o,a3,b3} on C3 and A4: {a3,a2,t} on A1 and A5: {a3,r,a1} on A2 and A6: {a2,s,a1} on A3 and A7: {t,b2,b3} on B1 and A8: {b1,r,b3} on B2 and A9: {b1,s,b2} on B3 and A10: C1,C2,C3 are_mutually_different and A11: o <> a3 and A12: o <> b1 and A13: o <> b2 and A14: a2 <> b2 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O A15: ( r on A2 & r on B2 ) by A5, A8, INCSP_1:2; A16: s on B3 by A9, INCSP_1:2; A17: a3 on A1 by A4, INCSP_1:2; A18: b3 on B1 by A7, INCSP_1:2; A19: b2 on B1 by A7, INCSP_1:2; A20: b3 on C3 by A3, INCSP_1:2; A21: a1 on C1 by A1, INCSP_1:2; A22: o on C2 by A2, INCSP_1:2; A23: s on A3 by A6, INCSP_1:2; A24: a1 on A3 by A6, INCSP_1:2; A25: a1 on A2 by A5, INCSP_1:2; A26: t on A1 by A4, INCSP_1:2; A27: b1 on B2 by A8, INCSP_1:2; A28: t on B1 by A7, INCSP_1:2; A29: b1 on B3 by A9, INCSP_1:2; A30: now__::_thesis:_(_o_<>_b3_&_o_<>_a1_&_o_<>_a2_&_a1_=_b1_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_) assume that o <> b3 and o <> a1 and o <> a2 and A31: a1 = b1 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O A32: now__::_thesis:_(_a3_<>_b3_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_) A33: b3 on B2 by A8, INCSP_1:2; consider O being LINE of IPP such that A34: ( t on O & s on O ) by INCPROJ:def_5; assume A35: a3 <> b3 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O take O = O; ::_thesis: {r,s,t} on O A36: ( b2 on C2 & o on C2 ) by A2, INCSP_1:2; A37: ( o on C1 & a2 on C2 ) by A1, A2, INCSP_1:2; A38: ( b1 on B3 & b2 on B3 ) by A9, INCSP_1:2; A39: ( b1 on A2 & a3 on A2 ) by A5, A31, INCSP_1:2; A40: ( a3 on C3 & b3 on C3 ) by A3, INCSP_1:2; A41: ( o on C1 & o on C3 ) by A1, A3, INCSP_1:2; A42: a2 on A3 by A6, INCSP_1:2; ( C1 <> C2 & b1 on C1 ) by A1, A10, INCSP_1:2, ZFMISC_1:def_5; then A3 <> B3 by A12, A14, A37, A36, A38, A42, Th10; then A43: b1 = s by A23, A24, A29, A16, A31, INCPROJ:def_4; ( C1 <> C3 & b1 on C1 ) by A1, A10, INCSP_1:2, ZFMISC_1:def_5; then A2 <> B2 by A12, A35, A41, A40, A39, A33, Th10; then s = r by A25, A27, A15, A31, A43, INCPROJ:def_4; hence {r,s,t} on O by A34, INCSP_1:2; ::_thesis: verum end; now__::_thesis:_(_a3_=_b3_implies_ex_B2_being_LINE_of_IPP_st_{r,s,t}_on_B2_) A44: ( a2 on A3 & b1 on A3 ) by A6, A31, INCSP_1:2; A45: ( C2 <> C3 & o on C2 ) by A2, A10, INCSP_1:2, ZFMISC_1:def_5; A46: ( a2 on C2 & b2 on C2 ) by A2, INCSP_1:2; A47: ( o on C1 & a2 on C2 ) by A1, A2, INCSP_1:2; A48: b2 on B3 by A9, INCSP_1:2; A49: ( a2 on A1 & b2 on B1 ) by A4, A7, INCSP_1:2; A50: ( o on C3 & b3 on C3 ) by A3, INCSP_1:2; assume A51: a3 = b3 ; ::_thesis: ex B2 being LINE of IPP st {r,s,t} on B2 then b3 on A1 by A4, INCSP_1:2; then A1 <> B1 by A11, A14, A51, A45, A46, A50, A49, Th10; then A52: t = b3 by A17, A26, A28, A18, A51, INCPROJ:def_4; take B2 = B2; ::_thesis: {r,s,t} on B2 A53: ( b2 on C2 & o on C2 ) by A2, INCSP_1:2; ( C1 <> C2 & b1 on C1 ) by A1, A10, INCSP_1:2, ZFMISC_1:def_5; then A3 <> B3 by A12, A14, A47, A53, A44, A48, Th10; then {s,r,t} on B2 by A8, A23, A24, A29, A16, A31, A52, INCPROJ:def_4; hence {r,s,t} on B2 by Th11; ::_thesis: verum end; hence ex O being LINE of IPP st {r,s,t} on O by A32; ::_thesis: verum end; A54: o on C1 by A1, INCSP_1:2; A55: C1 <> C2 by A10, ZFMISC_1:def_5; A56: b1 on C1 by A1, INCSP_1:2; A57: a2 on A3 by A6, INCSP_1:2; A58: b2 on C2 by A2, INCSP_1:2; A59: C2 <> C3 by A10, ZFMISC_1:def_5; A60: a3 on C3 by A3, INCSP_1:2; A61: b3 on B2 by A8, INCSP_1:2; A62: a3 on A2 by A5, INCSP_1:2; A63: a2 on A1 by A4, INCSP_1:2; A64: o on C3 by A3, INCSP_1:2; A65: b2 on B3 by A9, INCSP_1:2; A66: now__::_thesis:_(_o_<>_b3_&_o_<>_a1_&_o_=_a2_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_) assume that A67: o <> b3 and A68: o <> a1 and A69: o = a2 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O A70: now__::_thesis:_(_a1_=_b1_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_) assume A71: a1 = b1 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O A72: now__::_thesis:_(_a3_=_b3_implies_ex_B2_being_LINE_of_IPP_st_{r,s,t}_on_B2_) A73: ( a2 on A1 & b2 on B1 ) by A4, A7, INCSP_1:2; A74: ( b2 on C2 & b3 on C3 ) by A2, A3, INCSP_1:2; A75: ( b2 on C2 & a2 on A3 ) by A2, A6, INCSP_1:2; A76: ( o on C2 & b1 on C1 ) by A1, A2, INCSP_1:2; A77: ( C1 <> C2 & o on C1 ) by A1, A10, INCSP_1:2, ZFMISC_1:def_5; assume A78: a3 = b3 ; ::_thesis: ex B2 being LINE of IPP st {r,s,t} on B2 take B2 = B2; ::_thesis: {r,s,t} on B2 A79: b2 on B3 by A9, INCSP_1:2; ( b1 on A3 & a2 on C2 ) by A2, A6, A71, INCSP_1:2; then A3 <> B3 by A12, A14, A77, A76, A75, A79, Th10; then A80: s = b1 by A23, A24, A29, A16, A71, INCPROJ:def_4; A81: ( o on C3 & a2 on C2 ) by A2, A3, INCSP_1:2; A82: ( C2 <> C3 & o on C2 ) by A2, A10, INCSP_1:2, ZFMISC_1:def_5; b3 on A1 by A4, A78, INCSP_1:2; then A1 <> B1 by A11, A14, A78, A82, A81, A74, A73, Th10; then {s,r,t} on B2 by A8, A17, A26, A28, A18, A78, A80, INCPROJ:def_4; hence {r,s,t} on B2 by Th11; ::_thesis: verum end; now__::_thesis:_(_a3_<>_b3_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_) A83: ( o on C3 & a1 on C1 ) by A1, A3, INCSP_1:2; A84: ( a1 on A2 & a3 on A2 ) by A5, INCSP_1:2; A85: b3 on B2 by A8, INCSP_1:2; consider O being LINE of IPP such that A86: ( t on O & s on O ) by INCPROJ:def_5; assume A87: a3 <> b3 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O take O = O; ::_thesis: {r,s,t} on O A88: ( a3 on C3 & b3 on C3 ) by A3, INCSP_1:2; ( C1 <> C3 & o on C1 ) by A1, A10, INCSP_1:2, ZFMISC_1:def_5; then A2 <> B2 by A12, A71, A87, A83, A88, A84, A85, Th10; then A89: r = b1 by A25, A27, A15, A71, INCPROJ:def_4; ( A3 = C1 & B3 <> C1 ) by A13, A54, A21, A22, A58, A57, A24, A65, A55, A68, A69, INCPROJ:def_4; then r = s by A23, A24, A29, A16, A71, A89, INCPROJ:def_4; hence {r,s,t} on O by A86, INCSP_1:2; ::_thesis: verum end; hence ex O being LINE of IPP st {r,s,t} on O by A72; ::_thesis: verum end; now__::_thesis:_(_a1_<>_b1_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_) assume A90: a1 <> b1 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O A91: now__::_thesis:_(_a3_=_b3_implies_ex_O_being_Element_of_the_Lines_of_IPP_st_{r,s,t}_on_O_) A92: B1 <> C3 by A13, A22, A58, A64, A19, A59, INCPROJ:def_4; A93: ( o on C3 & a1 on C1 ) by A1, A3, INCSP_1:2; consider O being Element of the Lines of IPP such that A94: ( t on O & s on O ) by INCPROJ:def_5; A95: ( C1 <> C3 & o on C1 ) by A1, A10, INCSP_1:2, ZFMISC_1:def_5; A96: ( a1 on A2 & b1 on B2 ) by A5, A8, INCSP_1:2; A97: ( b1 on C1 & b3 on C3 ) by A1, A3, INCSP_1:2; assume A98: a3 = b3 ; ::_thesis: ex O being Element of the Lines of IPP st {r,s,t} on O then b3 on A2 by A5, INCSP_1:2; then A2 <> B2 by A11, A90, A98, A95, A93, A97, A96, Th10; then A99: r = b3 by A62, A15, A61, A98, INCPROJ:def_4; take O = O; ::_thesis: {r,s,t} on O A1 = C3 by A64, A60, A17, A63, A67, A69, A98, INCPROJ:def_4; then r = t by A20, A26, A28, A18, A92, A99, INCPROJ:def_4; hence {r,s,t} on O by A94, INCSP_1:2; ::_thesis: verum end; now__::_thesis:_(_a3_<>_b3_implies_ex_B2_being_LINE_of_IPP_st_{r,s,t}_on_B2_) assume a3 <> b3 ; ::_thesis: ex B2 being LINE of IPP st {r,s,t} on B2 take B2 = B2; ::_thesis: {r,s,t} on B2 ( A3 = C1 & B3 <> C1 ) by A13, A54, A21, A22, A58, A57, A24, A65, A55, A68, A69, INCPROJ:def_4; then A100: b1 = s by A56, A23, A29, A16, INCPROJ:def_4; ( A1 = C3 & B1 <> C3 ) by A11, A13, A22, A58, A64, A60, A17, A63, A19, A59, A69, INCPROJ:def_4; then {s,r,t} on B2 by A8, A20, A26, A28, A18, A100, INCPROJ:def_4; hence {r,s,t} on B2 by Th11; ::_thesis: verum end; hence ex O being LINE of IPP st {r,s,t} on O by A91; ::_thesis: verum end; hence ex O being LINE of IPP st {r,s,t} on O by A70; ::_thesis: verum end; A101: C3 <> C1 by A10, ZFMISC_1:def_5; A102: a2 on C2 by A2, INCSP_1:2; A103: now__::_thesis:_(_o_<>_b3_&_o_=_a1_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_) assume that A104: o <> b3 and A105: o = a1 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O A106: now__::_thesis:_(_o_<>_a2_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_) A107: now__::_thesis:_(_a3_=_b3_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_) A108: B2 <> C3 by A12, A54, A56, A64, A27, A101, INCPROJ:def_4; assume A109: a3 = b3 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O then A2 = C3 by A64, A60, A62, A25, A104, A105, INCPROJ:def_4; then A110: r = b3 by A20, A15, A61, A108, INCPROJ:def_4; A111: ( b2 on C2 & b3 on C3 ) by A2, A3, INCSP_1:2; A112: ( o on C3 & a2 on C2 ) by A2, A3, INCSP_1:2; A113: ( a2 on A1 & b2 on B1 ) by A4, A7, INCSP_1:2; consider O being LINE of IPP such that A114: ( t on O & s on O ) by INCPROJ:def_5; A115: ( C2 <> C3 & o on C2 ) by A2, A10, INCSP_1:2, ZFMISC_1:def_5; take O = O; ::_thesis: {r,s,t} on O b3 on A1 by A4, A109, INCSP_1:2; then A1 <> B1 by A11, A14, A109, A115, A112, A111, A113, Th10; then r = t by A17, A26, A28, A18, A109, A110, INCPROJ:def_4; hence {r,s,t} on O by A114, INCSP_1:2; ::_thesis: verum end; assume A116: o <> a2 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O now__::_thesis:_(_a3_<>_b3_implies_ex_B1_being_LINE_of_IPP_st_{r,s,t}_on_B1_) assume a3 <> b3 ; ::_thesis: ex B1 being LINE of IPP st {r,s,t} on B1 take B1 = B1; ::_thesis: {r,s,t} on B1 ( A3 = C2 & B3 <> C2 ) by A12, A54, A56, A22, A102, A57, A24, A29, A55, A105, A116, INCPROJ:def_4; then A117: s = b2 by A58, A23, A16, A65, INCPROJ:def_4; ( A2 = C3 & B2 <> C3 ) by A11, A12, A54, A56, A64, A60, A62, A25, A27, A101, A105, INCPROJ:def_4; then {t,s,r} on B1 by A7, A20, A15, A61, A117, INCPROJ:def_4; hence {r,s,t} on B1 by Th11; ::_thesis: verum end; hence ex O being LINE of IPP st {r,s,t} on O by A107; ::_thesis: verum end; now__::_thesis:_(_o_=_a2_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_) assume o = a2 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O then A118: A1 = C3 by A11, A64, A60, A17, A63, INCPROJ:def_4; ( A2 = C3 & B2 <> C3 ) by A11, A12, A54, A56, A64, A60, A62, A25, A27, A101, A105, INCPROJ:def_4; then A119: r = b3 by A20, A15, A61, INCPROJ:def_4; consider O being LINE of IPP such that A120: ( t on O & s on O ) by INCPROJ:def_5; take O = O; ::_thesis: {r,s,t} on O B1 <> C3 by A13, A22, A58, A64, A19, A59, INCPROJ:def_4; then r = t by A20, A26, A28, A18, A118, A119, INCPROJ:def_4; hence {r,s,t} on O by A120, INCSP_1:2; ::_thesis: verum end; hence ex O being LINE of IPP st {r,s,t} on O by A106; ::_thesis: verum end; A121: C1 <> B3 by A13, A54, A22, A58, A65, A55, INCPROJ:def_4; A122: now__::_thesis:_(_o_=_b3_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_) assume A123: o = b3 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O A124: now__::_thesis:_(_a1_=_o_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_) assume A125: a1 = o ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O A126: now__::_thesis:_(_o_=_a2_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_) assume o = a2 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O then A127: A1 = C3 by A11, A64, A60, A17, A63, INCPROJ:def_4; ( A2 = C3 & B2 = C1 ) by A11, A12, A54, A56, A64, A60, A62, A25, A27, A61, A123, A125, INCPROJ:def_4; then A128: o = r by A54, A64, A15, A101, INCPROJ:def_4; consider O being LINE of IPP such that A129: ( t on O & s on O ) by INCPROJ:def_5; take O = O; ::_thesis: {r,s,t} on O B1 = C2 by A13, A22, A58, A19, A18, A123, INCPROJ:def_4; then r = t by A22, A64, A26, A28, A59, A128, A127, INCPROJ:def_4; hence {r,s,t} on O by A129, INCSP_1:2; ::_thesis: verum end; now__::_thesis:_(_o_<>_a2_implies_ex_C2_being_LINE_of_IPP_st_{r,s,t}_on_C2_) ( B2 = C1 & A2 = C3 ) by A11, A12, A54, A56, A64, A60, A62, A25, A27, A61, A123, A125, INCPROJ:def_4; then A130: r = o by A54, A64, A15, A101, INCPROJ:def_4; assume o <> a2 ; ::_thesis: ex C2 being LINE of IPP st {r,s,t} on C2 then A131: C2 = A3 by A22, A102, A57, A24, A125, INCPROJ:def_4; take C2 = C2; ::_thesis: {r,s,t} on C2 C2 = B1 by A13, A22, A58, A19, A18, A123, INCPROJ:def_4; hence {r,s,t} on C2 by A22, A23, A28, A131, A130, INCSP_1:2; ::_thesis: verum end; hence ex O being LINE of IPP st {r,s,t} on O by A126; ::_thesis: verum end; now__::_thesis:_(_a1_<>_o_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_) assume A132: a1 <> o ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O A133: now__::_thesis:_(_o_=_a2_implies_ex_B2_being_LINE_of_IPP_st_{r,s,t}_on_B2_) assume A134: o = a2 ; ::_thesis: ex B2 being LINE of IPP st {r,s,t} on B2 then A135: A1 = C3 by A11, A64, A60, A17, A63, INCPROJ:def_4; take B2 = B2; ::_thesis: {r,s,t} on B2 C1 = A3 by A54, A21, A57, A24, A132, A134, INCPROJ:def_4; then A136: b1 = s by A56, A23, A29, A16, A121, INCPROJ:def_4; B1 = C2 by A13, A22, A58, A19, A18, A123, INCPROJ:def_4; then {s,r,t} on B2 by A8, A20, A26, A28, A18, A59, A136, A135, INCPROJ:def_4; hence {r,s,t} on B2 by Th11; ::_thesis: verum end; now__::_thesis:_(_o_<>_a2_implies_ex_A3_being_LINE_of_IPP_st_{r,s,t}_on_A3_) assume o <> a2 ; ::_thesis: ex A3 being LINE of IPP st {r,s,t} on A3 take A3 = A3; ::_thesis: {r,s,t} on A3 ( B2 = C1 & A2 <> C1 ) by A11, A12, A54, A56, A64, A60, A62, A27, A61, A101, A123, INCPROJ:def_4; then A137: r = a1 by A21, A25, A15, INCPROJ:def_4; ( B1 = C2 & A1 <> C2 ) by A11, A13, A22, A58, A64, A60, A17, A19, A18, A59, A123, INCPROJ:def_4; then {t,s,r} on A3 by A6, A102, A63, A26, A28, A137, INCPROJ:def_4; hence {r,s,t} on A3 by Th11; ::_thesis: verum end; hence ex O being LINE of IPP st {r,s,t} on O by A133; ::_thesis: verum end; hence ex O being LINE of IPP st {r,s,t} on O by A124; ::_thesis: verum end; now__::_thesis:_(_o_<>_b3_&_o_<>_a1_&_o_<>_a2_&_a1_<>_b1_&_a3_=_b3_implies_ex_O_being_Element_of_the_Lines_of_IPP_st_{r,s,t}_on_O_) A138: ( b2 on B1 & a2 on C2 ) by A2, A7, INCSP_1:2; A139: ( o on C3 & b3 on C3 ) by A3, INCSP_1:2; A140: ( a1 on A2 & b1 on B2 ) by A5, A8, INCSP_1:2; A141: ( b2 on C2 & o on C2 ) by A2, INCSP_1:2; A142: ( b3 on B1 & t on A1 ) by A4, A7, INCSP_1:2; A143: t on B1 by A7, INCSP_1:2; consider O being Element of the Lines of IPP such that A144: ( t on O & s on O ) by INCPROJ:def_5; assume that A145: o <> b3 and o <> a1 and o <> a2 and A146: a1 <> b1 and A147: a3 = b3 ; ::_thesis: ex O being Element of the Lines of IPP st {r,s,t} on O take O = O; ::_thesis: {r,s,t} on O A148: C1 <> C3 by A10, ZFMISC_1:def_5; b3 on A2 by A5, A147, INCSP_1:2; then A2 <> B2 by A54, A56, A21, A64, A20, A145, A146, A140, A148, Th10; then A149: b3 = r by A62, A15, A61, A147, INCPROJ:def_4; A150: b3 on A1 by A4, A147, INCSP_1:2; ( C2 <> C3 & a2 on A1 ) by A4, A10, INCSP_1:2, ZFMISC_1:def_5; then A1 <> B1 by A14, A145, A150, A138, A141, A139, Th10; then r = t by A150, A142, A143, A149, INCPROJ:def_4; hence {r,s,t} on O by A144, INCSP_1:2; ::_thesis: verum end; hence ex O being LINE of IPP st {r,s,t} on O by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A122, A103, A66, A30, INCPROJ:def_13; ::_thesis: verum end; Lm1: for IPP being IncProjSp for a, b, c, d being POINT of IPP for A, B being LINE of IPP st ex o being POINT of IPP st ( o on A & o on B ) & a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different holds ex p, q, r, s being POINT of IPP st ( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) proof let IPP be IncProjSp; ::_thesis: for a, b, c, d being POINT of IPP for A, B being LINE of IPP st ex o being POINT of IPP st ( o on A & o on B ) & a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different holds ex p, q, r, s being POINT of IPP st ( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) let a, b, c, d be POINT of IPP; ::_thesis: for A, B being LINE of IPP st ex o being POINT of IPP st ( o on A & o on B ) & a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different holds ex p, q, r, s being POINT of IPP st ( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) let A, B be LINE of IPP; ::_thesis: ( ex o being POINT of IPP st ( o on A & o on B ) & a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different implies ex p, q, r, s being POINT of IPP st ( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) ) assume that A1: ex o being POINT of IPP st ( o on A & o on B ) and A2: a on A and A3: b on A and A4: c on A and A5: d on A and A6: a,b,c,d are_mutually_different ; ::_thesis: ex p, q, r, s being POINT of IPP st ( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) consider o being POINT of IPP such that A7: o on A and A8: o on B by A1; now__::_thesis:_(_A_<>_B_implies_ex_p,_q,_r,_s_being_POINT_of_IPP_st_ (_p_on_B_&_q_on_B_&_r_on_B_&_s_on_B_&_p,q,r,s_are_mutually_different_)_) assume A <> B ; ::_thesis: ex p, q, r, s being POINT of IPP st ( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) then consider x, y being POINT of IPP such that A9: x on A and A10: not x on B and A11: y on B and A12: not y on A by Th3; consider C being LINE of IPP such that A13: x on C and A14: y on C by INCPROJ:def_5; consider w being POINT of IPP such that A15: w on C and A16: w <> x and A17: w <> y by Th8; A18: now__::_thesis:_for_u1,_u2,_v1,_v2_being_POINT_of_IPP for_D1,_D2_being_LINE_of_IPP_st_u1_on_A_&_u2_on_A_&_v1_on_B_&_w_on_D1_&_u1_on_D1_&_v1_on_D1_&_v2_on_B_&_w_on_D2_&_u2_on_D2_&_v2_on_D2_&_u1_<>_u2_holds_ not_v1_=_v2 A19: not w on B by A10, A11, A13, A14, A15, A17, INCPROJ:def_4; let u1, u2, v1, v2 be POINT of IPP; ::_thesis: for D1, D2 being LINE of IPP st u1 on A & u2 on A & v1 on B & w on D1 & u1 on D1 & v1 on D1 & v2 on B & w on D2 & u2 on D2 & v2 on D2 & u1 <> u2 holds not v1 = v2 let D1, D2 be LINE of IPP; ::_thesis: ( u1 on A & u2 on A & v1 on B & w on D1 & u1 on D1 & v1 on D1 & v2 on B & w on D2 & u2 on D2 & v2 on D2 & u1 <> u2 implies not v1 = v2 ) assume that A20: ( u1 on A & u2 on A ) and A21: v1 on B and A22: w on D1 and A23: u1 on D1 and A24: v1 on D1 and v2 on B and A25: w on D2 and A26: u2 on D2 and A27: v2 on D2 ; ::_thesis: ( u1 <> u2 implies not v1 = v2 ) A28: D1 <> A by A9, A12, A13, A14, A15, A16, A22, INCPROJ:def_4; assume A29: u1 <> u2 ; ::_thesis: not v1 = v2 assume v1 = v2 ; ::_thesis: contradiction then D1 = D2 by A21, A22, A24, A25, A27, A19, INCPROJ:def_4; hence contradiction by A20, A23, A26, A29, A28, INCPROJ:def_4; ::_thesis: verum end; A30: now__::_thesis:_for_u_being_POINT_of_IPP_st_u_on_A_holds_ ex_v_being_POINT_of_IPP_ex_D_being_LINE_of_IPP_st_ (_v_on_B_&_w_on_D_&_u_on_D_&_v_on_D_) let u be POINT of IPP; ::_thesis: ( u on A implies ex v being POINT of IPP ex D being LINE of IPP st ( v on B & w on D & u on D & v on D ) ) assume A31: u on A ; ::_thesis: ex v being POINT of IPP ex D being LINE of IPP st ( v on B & w on D & u on D & v on D ) A32: now__::_thesis:_(_u_<>_o_&_x_<>_u_implies_ex_v_being_POINT_of_IPP_ex_D_being_LINE_of_IPP_st_ (_v_on_B_&_w_on_D_&_u_on_D_&_v_on_D_)_) assume that u <> o and A33: x <> u ; ::_thesis: ex v being POINT of IPP ex D being LINE of IPP st ( v on B & w on D & u on D & v on D ) consider D being LINE of IPP such that A34: ( w on D & u on D ) by INCPROJ:def_5; not x on D proof assume x on D ; ::_thesis: contradiction then u on C by A13, A15, A16, A34, INCPROJ:def_4; hence contradiction by A9, A12, A13, A14, A31, A33, INCPROJ:def_4; ::_thesis: verum end; then consider v being POINT of IPP such that A35: ( v on B & v on D ) by A7, A8, A9, A10, A11, A12, A13, A14, A15, A31, A34, INCPROJ:def_8; take v = v; ::_thesis: ex D being LINE of IPP st ( v on B & w on D & u on D & v on D ) take D = D; ::_thesis: ( v on B & w on D & u on D & v on D ) thus ( v on B & w on D & u on D & v on D ) by A34, A35; ::_thesis: verum end; now__::_thesis:_(_u_=_o_implies_ex_v_being_POINT_of_IPP_ex_D_being_LINE_of_IPP_st_ (_v_on_B_&_w_on_D_&_u_on_D_&_v_on_D_)_) consider D being LINE of IPP such that A36: ( w on D & u on D ) by INCPROJ:def_5; assume A37: u = o ; ::_thesis: ex v being POINT of IPP ex D being LINE of IPP st ( v on B & w on D & u on D & v on D ) take v = o; ::_thesis: ex D being LINE of IPP st ( v on B & w on D & u on D & v on D ) take D = D; ::_thesis: ( v on B & w on D & u on D & v on D ) thus ( v on B & w on D & u on D & v on D ) by A8, A37, A36; ::_thesis: verum end; hence ex v being POINT of IPP ex D being LINE of IPP st ( v on B & w on D & u on D & v on D ) by A11, A13, A14, A15, A32; ::_thesis: verum end; then consider p being POINT of IPP, D1 being Element of the Lines of IPP such that A38: p on B and A39: ( w on D1 & a on D1 & p on D1 ) by A2; consider r being POINT of IPP, D3 being Element of the Lines of IPP such that A40: r on B and A41: ( w on D3 & c on D3 & r on D3 ) by A4, A30; consider q being POINT of IPP, D2 being Element of the Lines of IPP such that A42: q on B and A43: ( w on D2 & b on D2 & q on D2 ) by A3, A30; consider s being POINT of IPP, D4 being Element of the Lines of IPP such that A44: s on B and A45: ( w on D4 & d on D4 & s on D4 ) by A5, A30; d <> a by A6, ZFMISC_1:def_6; then A46: s <> p by A2, A5, A18, A38, A39, A45; a <> c by A6, ZFMISC_1:def_6; then A47: p <> r by A2, A4, A18, A38, A39, A41; d <> b by A6, ZFMISC_1:def_6; then A48: s <> q by A3, A5, A18, A42, A43, A45; c <> d by A6, ZFMISC_1:def_6; then A49: r <> s by A4, A5, A18, A40, A41, A45; b <> c by A6, ZFMISC_1:def_6; then A50: q <> r by A3, A4, A18, A42, A43, A41; a <> b by A6, ZFMISC_1:def_6; then p <> q by A2, A3, A18, A38, A39, A43; then p,q,r,s are_mutually_different by A50, A49, A46, A48, A47, ZFMISC_1:def_6; hence ex p, q, r, s being POINT of IPP st ( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) by A38, A42, A40, A44; ::_thesis: verum end; hence ex p, q, r, s being POINT of IPP st ( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) by A2, A3, A4, A5, A6; ::_thesis: verum end; theorem Th13: :: PROJRED1:13 for IPP being IncProjSp st ex A being LINE of IPP ex a, b, c, d being POINT of IPP st ( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different ) holds for B being LINE of IPP ex p, q, r, s being POINT of IPP st ( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) proof let IPP be IncProjSp; ::_thesis: ( ex A being LINE of IPP ex a, b, c, d being POINT of IPP st ( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different ) implies for B being LINE of IPP ex p, q, r, s being POINT of IPP st ( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) ) given A being LINE of IPP, a, b, c, d being POINT of IPP such that A1: ( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different ) ; ::_thesis: for B being LINE of IPP ex p, q, r, s being POINT of IPP st ( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) let B be LINE of IPP; ::_thesis: ex p, q, r, s being POINT of IPP st ( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) consider x being POINT of IPP such that A2: x on A by Th7; consider y being POINT of IPP such that A3: y on B by Th7; consider C being LINE of IPP such that A4: x on C and A5: y on C by INCPROJ:def_5; ex p1, q1, r1, s1 being POINT of IPP st ( p1 on C & q1 on C & r1 on C & s1 on C & p1,q1,r1,s1 are_mutually_different ) by A1, A2, A4, Lm1; hence ex p, q, r, s being POINT of IPP st ( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) by A3, A5, Lm1; ::_thesis: verum end; Lm2: for IPP being Fanoian IncProjSp ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP ex d being POINT of IPP st ( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C & b on D & c on D & C,D,R,S are_mutually_different & d on A & c,d,p,q are_mutually_different ) proof let IPP be Fanoian IncProjSp; ::_thesis: ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP ex d being POINT of IPP st ( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C & b on D & c on D & C,D,R,S are_mutually_different & d on A & c,d,p,q are_mutually_different ) consider r being POINT of IPP, A being LINE of IPP such that A1: not r on A by INCPROJ:def_6; consider p, q, c being POINT of IPP such that A2: p <> q and A3: q <> c and A4: c <> p and A5: p on A and A6: q on A and A7: c on A by INCPROJ:def_7; consider B being LINE of IPP such that A8: r on B and A9: c on B by INCPROJ:def_5; consider s being POINT of IPP such that A10: s on B and A11: s <> r and A12: s <> c by Th8; consider L being LINE of IPP such that A13: p on L and A14: s on L by INCPROJ:def_5; consider Q being LINE of IPP such that A15: r on Q and A16: q on Q by INCPROJ:def_5; A17: not p on Q by A1, A2, A5, A6, A15, A16, INCPROJ:def_4; A18: not c on Q by A1, A3, A6, A7, A15, A16, INCPROJ:def_4; then A19: not s on Q by A8, A9, A10, A11, A15, INCPROJ:def_4; not c on L proof assume c on L ; ::_thesis: contradiction then p on B by A9, A10, A12, A13, A14, INCPROJ:def_4; hence contradiction by A1, A4, A5, A7, A8, A9, INCPROJ:def_4; ::_thesis: verum end; then consider a being POINT of IPP such that A20: a on Q and A21: a on L by A1, A5, A6, A7, A8, A9, A10, A15, A16, A13, A14, A18, INCPROJ:def_8; A22: {a,p,s} on L by A13, A14, A21, INCSP_1:2; consider R being LINE of IPP such that A23: q on R and A24: s on R by INCPROJ:def_5; consider S being LINE of IPP such that A25: p on S and A26: r on S by INCPROJ:def_5; A27: not c on S by A1, A4, A5, A7, A25, A26, INCPROJ:def_4; then A28: not s on S by A8, A9, A10, A11, A26, INCPROJ:def_4; A29: S <> L by A8, A9, A10, A11, A14, A26, A27, INCPROJ:def_4; then A30: not r on L by A1, A5, A13, A25, A26, INCPROJ:def_4; A31: S <> Q by A1, A2, A5, A6, A15, A16, A25, INCPROJ:def_4; A32: not q on S by A1, A2, A5, A6, A25, A26, INCPROJ:def_4; A33: not q on L proof assume q on L ; ::_thesis: contradiction then s on A by A2, A5, A6, A13, A14, INCPROJ:def_4; hence contradiction by A1, A7, A8, A9, A10, A12, INCPROJ:def_4; ::_thesis: verum end; A34: not p on R proof assume p on R ; ::_thesis: contradiction then s on A by A2, A5, A6, A23, A24, INCPROJ:def_4; hence contradiction by A1, A7, A8, A9, A10, A12, INCPROJ:def_4; ::_thesis: verum end; then not c on R by A3, A5, A6, A7, A23, INCPROJ:def_4; then consider b being POINT of IPP such that A35: b on R and A36: b on S by A1, A5, A6, A7, A8, A9, A10, A25, A26, A23, A24, A27, INCPROJ:def_8; A37: {b,q,s} on R by A23, A24, A35, INCSP_1:2; A38: R <> Q proof assume not R <> Q ; ::_thesis: contradiction then B = Q by A8, A10, A11, A15, A24, INCPROJ:def_4; hence contradiction by A1, A3, A6, A7, A8, A9, A16, INCPROJ:def_4; ::_thesis: verum end; then A39: not r on R by A1, A6, A15, A16, A23, INCPROJ:def_4; A40: {c,r,s} on B by A8, A9, A10, INCSP_1:2; A41: {b,p,r} on S by A25, A26, A36, INCSP_1:2; A42: a <> r by A1, A5, A13, A25, A26, A21, A29, INCPROJ:def_4; then A43: not a on S by A15, A16, A26, A32, A20, INCPROJ:def_4; A44: {a,q,r} on Q by A15, A16, A20, INCSP_1:2; consider C being LINE of IPP such that A45: a on C and A46: b on C by INCPROJ:def_5; a <> s by A8, A9, A10, A11, A15, A18, A20, INCPROJ:def_4; then A47: R <> C by A13, A14, A24, A34, A21, A45, INCPROJ:def_4; A48: not b on Q by A16, A23, A38, A32, A35, A36, INCPROJ:def_4; then not r on C by A15, A20, A45, A46, A42, INCPROJ:def_4; then consider d being POINT of IPP such that A49: d on A and A50: d on C by A1, A5, A6, A15, A16, A25, A26, A20, A36, A45, A46, A31, INCPROJ:def_8; S <> C by A15, A16, A26, A32, A20, A45, A42, INCPROJ:def_4; then A51: d <> p by A25, A34, A35, A36, A46, A50, INCPROJ:def_4; A52: {c,p,q} on A by A5, A6, A7, INCSP_1:2; A53: {a,b} on C by A45, A46, INCSP_1:1; then A54: not c on C by A39, A17, A32, A33, A34, A19, A30, A28, A22, A44, A37, A41, A52, A40, INCPROJ:def_12; consider D being LINE of IPP such that A55: b on D and A56: c on D by INCPROJ:def_5; A57: R <> D by A3, A5, A6, A7, A23, A34, A56, INCPROJ:def_4; d <> q by A16, A33, A20, A21, A45, A46, A48, A50, INCPROJ:def_4; then A58: c,d,p,q are_mutually_different by A2, A3, A4, A54, A50, A51, ZFMISC_1:def_6; S <> D by A1, A4, A5, A7, A25, A26, A56, INCPROJ:def_4; then C,D,R,S are_mutually_different by A25, A34, A45, A54, A56, A43, A57, A47, ZFMISC_1:def_6; hence ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP ex d being POINT of IPP st ( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C & b on D & c on D & C,D,R,S are_mutually_different & d on A & c,d,p,q are_mutually_different ) by A39, A17, A32, A33, A34, A19, A30, A28, A22, A44, A37, A41, A52, A40, A53, A54, A55, A56, A49, A58; ::_thesis: verum end; theorem :: PROJRED1:14 for IPP being Fanoian IncProjSp ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP st ( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C ) proof let IPP be Fanoian IncProjSp; ::_thesis: ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP st ( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C ) ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP ex d being POINT of IPP st ( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C & b on D & c on D & C,D,R,S are_mutually_different & d on A & c,d,p,q are_mutually_different ) by Lm2; hence ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP st ( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C ) ; ::_thesis: verum end; theorem :: PROJRED1:15 for IPP being Fanoian IncProjSp ex a being POINT of IPP ex A, B, C, D being LINE of IPP st ( a on A & a on B & a on C & a on D & A,B,C,D are_mutually_different ) proof let IPP be Fanoian IncProjSp; ::_thesis: ex a being POINT of IPP ex A, B, C, D being LINE of IPP st ( a on A & a on B & a on C & a on D & A,B,C,D are_mutually_different ) consider p, q, r, s, a, b, c being POINT of IPP, A, B, C, Q, L, R, S, D being LINE of IPP, d being POINT of IPP such that not q on L and not r on L and not p on Q and not s on Q and not p on R and not r on R and not q on S and not s on S and {a,p,s} on L and {a,q,r} on Q and A1: ( {b,q,s} on R & {b,p,r} on S ) and {c,p,q} on A and {c,r,s} on B and A2: {a,b} on C and not c on C and A3: b on D and c on D and A4: C,D,R,S are_mutually_different and d on A and c,d,p,q are_mutually_different by Lm2; A5: b on C by A2, INCSP_1:1; ( b on S & b on R ) by A1, INCSP_1:2; hence ex a being POINT of IPP ex A, B, C, D being LINE of IPP st ( a on A & a on B & a on C & a on D & A,B,C,D are_mutually_different ) by A3, A4, A5; ::_thesis: verum end; theorem Th16: :: PROJRED1:16 for IPP being Fanoian IncProjSp ex a, b, c, d being POINT of IPP ex A being LINE of IPP st ( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different ) proof let IPP be Fanoian IncProjSp; ::_thesis: ex a, b, c, d being POINT of IPP ex A being LINE of IPP st ( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different ) consider p, q, r, s, a, b, c being POINT of IPP, A, B, C, Q, L, R, S, D being LINE of IPP, d being POINT of IPP such that not q on L and not r on L and not p on Q and not s on Q and not p on R and not r on R and not q on S and not s on S and {a,p,s} on L and {a,q,r} on Q and {b,q,s} on R and {b,p,r} on S and A1: {c,p,q} on A and {c,r,s} on B and {a,b} on C and not c on C and b on D and c on D and C,D,R,S are_mutually_different and A2: ( d on A & c,d,p,q are_mutually_different ) by Lm2; A3: q on A by A1, INCSP_1:2; ( c on A & p on A ) by A1, INCSP_1:2; hence ex a, b, c, d being POINT of IPP ex A being LINE of IPP st ( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different ) by A2, A3; ::_thesis: verum end; theorem :: PROJRED1:17 for IPP being Fanoian IncProjSp for B being LINE of IPP ex p, q, r, s being POINT of IPP st ( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) proof let IPP be Fanoian IncProjSp; ::_thesis: for B being LINE of IPP ex p, q, r, s being POINT of IPP st ( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) let B be LINE of IPP; ::_thesis: ex p, q, r, s being POINT of IPP st ( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) ex a, b, c, d being POINT of IPP ex A being LINE of IPP st ( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different ) by Th16; hence ex p, q, r, s being POINT of IPP st ( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) by Th13; ::_thesis: verum end; definition let IPP be 2-dimensional Desarguesian IncProjSp; let K, L be LINE of IPP; let p be POINT of IPP; assume that A1: not p on K and A2: not p on L ; func IncProj (K,p,L) -> PartFunc of the Points of IPP, the Points of IPP means :Def1: :: PROJRED1:def 1 ( dom it c= the Points of IPP & ( for x being POINT of IPP holds ( x in dom it iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds ( it . x = y iff ex X being LINE of IPP st ( p on X & x on X & y on X ) ) ) ); existence ex b1 being PartFunc of the Points of IPP, the Points of IPP st ( dom b1 c= the Points of IPP & ( for x being POINT of IPP holds ( x in dom b1 iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds ( b1 . x = y iff ex X being LINE of IPP st ( p on X & x on X & y on X ) ) ) ) proof defpred S1[ set , set ] means ex x, y being POINT of IPP st ( x = $1 & y = $2 & x on K & y on L & ex X being LINE of IPP st ( p on X & x on X & y on X ) ); set XX = the Points of IPP; A3: for x, y1, y2 being set st x in the Points of IPP & S1[x,y1] & S1[x,y2] holds y1 = y2 proof let x, y1, y2 be set ; ::_thesis: ( x in the Points of IPP & S1[x,y1] & S1[x,y2] implies y1 = y2 ) assume that A4: x in the Points of IPP and A5: S1[x,y1] and A6: S1[x,y2] ; ::_thesis: y1 = y2 reconsider x = x as POINT of IPP by A4; reconsider y1 = y1, y2 = y2 as POINT of IPP by A5, A6; consider A1 being Element of the Lines of IPP such that A7: p on A1 and A8: x on A1 and A9: y1 on A1 by A5; y2 on A1 by A1, A6, A7, A8, INCPROJ:def_4; hence y1 = y2 by A2, A5, A6, A7, A9, INCPROJ:def_4; ::_thesis: verum end; A10: for x, y being set st x in the Points of IPP & S1[x,y] holds y in the Points of IPP ; consider f being PartFunc of the Points of IPP, the Points of IPP such that A11: for x being set holds ( x in dom f iff ( x in the Points of IPP & ex y being set st S1[x,y] ) ) and A12: for x being set st x in dom f holds S1[x,f . x] from PARTFUN1:sch_2(A10, A3); take f ; ::_thesis: ( dom f c= the Points of IPP & ( for x being POINT of IPP holds ( x in dom f iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds ( f . x = y iff ex X being LINE of IPP st ( p on X & x on X & y on X ) ) ) ) thus dom f c= the Points of IPP ; ::_thesis: ( ( for x being POINT of IPP holds ( x in dom f iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds ( f . x = y iff ex X being LINE of IPP st ( p on X & x on X & y on X ) ) ) ) thus A13: for x being POINT of IPP holds ( x in dom f iff x on K ) ::_thesis: for x, y being POINT of IPP st x on K & y on L holds ( f . x = y iff ex X being LINE of IPP st ( p on X & x on X & y on X ) ) proof let x be POINT of IPP; ::_thesis: ( x in dom f iff x on K ) A14: ( x on K implies x in dom f ) proof consider X being LINE of IPP such that A15: ( p on X & x on X ) by INCPROJ:def_5; assume A16: x on K ; ::_thesis: x in dom f ex y being POINT of IPP st ( y on L & y on X ) by INCPROJ:def_9; hence x in dom f by A11, A16, A15; ::_thesis: verum end; ( x in dom f implies x on K ) proof assume x in dom f ; ::_thesis: x on K then S1[x,f . x] by A12; hence x on K ; ::_thesis: verum end; hence ( x in dom f iff x on K ) by A14; ::_thesis: verum end; let x, y be POINT of IPP; ::_thesis: ( x on K & y on L implies ( f . x = y iff ex X being LINE of IPP st ( p on X & x on X & y on X ) ) ) assume that A17: x on K and A18: y on L ; ::_thesis: ( f . x = y iff ex X being LINE of IPP st ( p on X & x on X & y on X ) ) A19: ( f . x = y implies ex X being LINE of IPP st ( p on X & x on X & y on X ) ) proof x in dom f by A13, A17; then A20: S1[x,f . x] by A12; assume f . x = y ; ::_thesis: ex X being LINE of IPP st ( p on X & x on X & y on X ) hence ex X being LINE of IPP st ( p on X & x on X & y on X ) by A20; ::_thesis: verum end; ( ex X being LINE of IPP st ( p on X & x on X & y on X ) implies f . x = y ) proof x in dom f by A13, A17; then A21: S1[x,f . x] by A12; assume ex X being LINE of IPP st ( p on X & x on X & y on X ) ; ::_thesis: f . x = y hence f . x = y by A3, A18, A21; ::_thesis: verum end; hence ( f . x = y iff ex X being LINE of IPP st ( p on X & x on X & y on X ) ) by A19; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of the Points of IPP, the Points of IPP st dom b1 c= the Points of IPP & ( for x being POINT of IPP holds ( x in dom b1 iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds ( b1 . x = y iff ex X being LINE of IPP st ( p on X & x on X & y on X ) ) ) & dom b2 c= the Points of IPP & ( for x being POINT of IPP holds ( x in dom b2 iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds ( b2 . x = y iff ex X being LINE of IPP st ( p on X & x on X & y on X ) ) ) holds b1 = b2 proof let f1, f2 be PartFunc of the Points of IPP, the Points of IPP; ::_thesis: ( dom f1 c= the Points of IPP & ( for x being POINT of IPP holds ( x in dom f1 iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds ( f1 . x = y iff ex X being LINE of IPP st ( p on X & x on X & y on X ) ) ) & dom f2 c= the Points of IPP & ( for x being POINT of IPP holds ( x in dom f2 iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds ( f2 . x = y iff ex X being LINE of IPP st ( p on X & x on X & y on X ) ) ) implies f1 = f2 ) assume that dom f1 c= the Points of IPP and A22: for x being POINT of IPP holds ( x in dom f1 iff x on K ) and A23: for x, y being POINT of IPP st x on K & y on L holds ( f1 . x = y iff ex X being LINE of IPP st ( p on X & x on X & y on X ) ) and dom f2 c= the Points of IPP and A24: for x being POINT of IPP holds ( x in dom f2 iff x on K ) and A25: for x, y being POINT of IPP st x on K & y on L holds ( f2 . x = y iff ex X being LINE of IPP st ( p on X & x on X & y on X ) ) ; ::_thesis: f1 = f2 for x being set holds ( x in dom f1 iff x in dom f2 ) proof let x be set ; ::_thesis: ( x in dom f1 iff x in dom f2 ) A26: ( x in dom f2 implies x in dom f1 ) proof assume A27: x in dom f2 ; ::_thesis: x in dom f1 then reconsider x = x as Element of the Points of IPP ; x on K by A24, A27; hence x in dom f1 by A22; ::_thesis: verum end; ( x in dom f1 implies x in dom f2 ) proof assume A28: x in dom f1 ; ::_thesis: x in dom f2 then reconsider x = x as Element of the Points of IPP ; x on K by A22, A28; hence x in dom f2 by A24; ::_thesis: verum end; hence ( x in dom f1 iff x in dom f2 ) by A26; ::_thesis: verum end; then A29: dom f1 = dom f2 by TARSKI:1; for x being POINT of IPP st x in dom f1 holds f1 . x = f2 . x proof let x be POINT of IPP; ::_thesis: ( x in dom f1 implies f1 . x = f2 . x ) consider A2 being LINE of IPP such that A30: ( p on A2 & x on A2 ) by INCPROJ:def_5; consider y2 being POINT of IPP such that A31: ( y2 on A2 & y2 on L ) by INCPROJ:def_9; assume x in dom f1 ; ::_thesis: f1 . x = f2 . x then A32: x on K by A22; then f2 . x = y2 by A25, A30, A31; hence f1 . x = f2 . x by A23, A32, A30, A31; ::_thesis: verum end; hence f1 = f2 by A29, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def1 defines IncProj PROJRED1:def_1_:_ for IPP being 2-dimensional Desarguesian IncProjSp for K, L being LINE of IPP for p being POINT of IPP st not p on K & not p on L holds for b5 being PartFunc of the Points of IPP, the Points of IPP holds ( b5 = IncProj (K,p,L) iff ( dom b5 c= the Points of IPP & ( for x being POINT of IPP holds ( x in dom b5 iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds ( b5 . x = y iff ex X being LINE of IPP st ( p on X & x on X & y on X ) ) ) ) ); theorem Th18: :: PROJRED1:18 for IPP being 2-dimensional Desarguesian IncProjSp for p being POINT of IPP for K being LINE of IPP st not p on K holds for x being POINT of IPP st x on K holds (IncProj (K,p,K)) . x = x proof let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for p being POINT of IPP for K being LINE of IPP st not p on K holds for x being POINT of IPP st x on K holds (IncProj (K,p,K)) . x = x let p be POINT of IPP; ::_thesis: for K being LINE of IPP st not p on K holds for x being POINT of IPP st x on K holds (IncProj (K,p,K)) . x = x let K be LINE of IPP; ::_thesis: ( not p on K implies for x being POINT of IPP st x on K holds (IncProj (K,p,K)) . x = x ) assume A1: not p on K ; ::_thesis: for x being POINT of IPP st x on K holds (IncProj (K,p,K)) . x = x let x be POINT of IPP; ::_thesis: ( x on K implies (IncProj (K,p,K)) . x = x ) A2: ex X being LINE of IPP st ( p on X & x on X ) by INCPROJ:def_5; assume x on K ; ::_thesis: (IncProj (K,p,K)) . x = x hence (IncProj (K,p,K)) . x = x by A1, A2, Def1; ::_thesis: verum end; theorem Th19: :: PROJRED1:19 for IPP being 2-dimensional Desarguesian IncProjSp for p, x being POINT of IPP for K, L being LINE of IPP st not p on K & not p on L & x on K holds (IncProj (K,p,L)) . x is POINT of IPP proof let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for p, x being POINT of IPP for K, L being LINE of IPP st not p on K & not p on L & x on K holds (IncProj (K,p,L)) . x is POINT of IPP let p, x be POINT of IPP; ::_thesis: for K, L being LINE of IPP st not p on K & not p on L & x on K holds (IncProj (K,p,L)) . x is POINT of IPP let K, L be LINE of IPP; ::_thesis: ( not p on K & not p on L & x on K implies (IncProj (K,p,L)) . x is POINT of IPP ) assume ( not p on K & not p on L & x on K ) ; ::_thesis: (IncProj (K,p,L)) . x is POINT of IPP then x in dom (IncProj (K,p,L)) by Def1; hence (IncProj (K,p,L)) . x is POINT of IPP by PARTFUN1:4; ::_thesis: verum end; theorem Th20: :: PROJRED1:20 for IPP being 2-dimensional Desarguesian IncProjSp for p, x, y being POINT of IPP for K, L being LINE of IPP st not p on K & not p on L & x on K & y = (IncProj (K,p,L)) . x holds y on L proof let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for p, x, y being POINT of IPP for K, L being LINE of IPP st not p on K & not p on L & x on K & y = (IncProj (K,p,L)) . x holds y on L let p, x, y be POINT of IPP; ::_thesis: for K, L being LINE of IPP st not p on K & not p on L & x on K & y = (IncProj (K,p,L)) . x holds y on L let K, L be LINE of IPP; ::_thesis: ( not p on K & not p on L & x on K & y = (IncProj (K,p,L)) . x implies y on L ) assume A1: ( not p on K & not p on L & x on K & y = (IncProj (K,p,L)) . x ) ; ::_thesis: y on L consider X being LINE of IPP such that A2: ( p on X & x on X ) by INCPROJ:def_5; ex z being POINT of IPP st ( z on L & z on X ) by INCPROJ:def_9; hence y on L by A1, A2, Def1; ::_thesis: verum end; theorem :: PROJRED1:21 for IPP being 2-dimensional Desarguesian IncProjSp for p, y being POINT of IPP for K, L being LINE of IPP st not p on K & not p on L & y in rng (IncProj (K,p,L)) holds y on L proof let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for p, y being POINT of IPP for K, L being LINE of IPP st not p on K & not p on L & y in rng (IncProj (K,p,L)) holds y on L let p, y be POINT of IPP; ::_thesis: for K, L being LINE of IPP st not p on K & not p on L & y in rng (IncProj (K,p,L)) holds y on L let K, L be LINE of IPP; ::_thesis: ( not p on K & not p on L & y in rng (IncProj (K,p,L)) implies y on L ) assume that A1: ( not p on K & not p on L ) and A2: y in rng (IncProj (K,p,L)) ; ::_thesis: y on L consider x being POINT of IPP such that A3: x in dom (IncProj (K,p,L)) and A4: y = (IncProj (K,p,L)) . x by A2, PARTFUN1:3; x on K by A1, A3, Def1; hence y on L by A1, A4, Th20; ::_thesis: verum end; theorem Th22: :: PROJRED1:22 for IPP being 2-dimensional Desarguesian IncProjSp for p, q being POINT of IPP for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R holds ( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) ) proof let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for p, q being POINT of IPP for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R holds ( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) ) let p, q be POINT of IPP; ::_thesis: for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R holds ( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) ) let K, L, R be LINE of IPP; ::_thesis: ( not p on K & not p on L & not q on L & not q on R implies ( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) ) ) assume that A1: ( not p on K & not p on L ) and A2: ( not q on L & not q on R ) ; ::_thesis: ( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) ) for x being set holds ( x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) iff x in dom (IncProj (K,p,L)) ) proof let x be set ; ::_thesis: ( x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) iff x in dom (IncProj (K,p,L)) ) ( x in dom (IncProj (K,p,L)) implies x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) ) proof assume A3: x in dom (IncProj (K,p,L)) ; ::_thesis: x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) then reconsider x9 = x as POINT of IPP ; consider A being LINE of IPP such that A4: ( x9 on A & p on A ) by INCPROJ:def_5; consider y being POINT of IPP such that A5: y on A and A6: y on L by INCPROJ:def_9; A7: y in dom (IncProj (L,q,R)) by A2, A6, Def1; x9 on K by A1, A3, Def1; then (IncProj (K,p,L)) . x = y by A1, A4, A5, A6, Def1; hence x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A3, A7, FUNCT_1:11; ::_thesis: verum end; hence ( x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) iff x in dom (IncProj (K,p,L)) ) by FUNCT_1:11; ::_thesis: verum end; hence dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by TARSKI:1; ::_thesis: rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) for x being set st x in dom (IncProj (L,q,R)) holds x in rng (IncProj (K,p,L)) proof let x be set ; ::_thesis: ( x in dom (IncProj (L,q,R)) implies x in rng (IncProj (K,p,L)) ) assume A8: x in dom (IncProj (L,q,R)) ; ::_thesis: x in rng (IncProj (K,p,L)) thus x in rng (IncProj (K,p,L)) ::_thesis: verum proof reconsider x9 = x as POINT of IPP by A8; A9: x9 on L by A2, A8, Def1; ex y being POINT of IPP st ( y in dom (IncProj (K,p,L)) & x9 = (IncProj (K,p,L)) . y ) proof consider A being LINE of IPP such that A10: ( x9 on A & p on A ) by INCPROJ:def_5; consider y being POINT of IPP such that A11: y on A and A12: y on K by INCPROJ:def_9; take y ; ::_thesis: ( y in dom (IncProj (K,p,L)) & x9 = (IncProj (K,p,L)) . y ) thus y in dom (IncProj (K,p,L)) by A1, A12, Def1; ::_thesis: x9 = (IncProj (K,p,L)) . y thus x9 = (IncProj (K,p,L)) . y by A1, A9, A10, A11, A12, Def1; ::_thesis: verum end; hence x in rng (IncProj (K,p,L)) by FUNCT_1:def_3; ::_thesis: verum end; end; then dom (IncProj (L,q,R)) c= rng (IncProj (K,p,L)) by TARSKI:def_3; hence rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) by RELAT_1:28; ::_thesis: verum end; theorem Th23: :: PROJRED1:23 for IPP being 2-dimensional Desarguesian IncProjSp for p being POINT of IPP for K, L being LINE of IPP for a1, b1, a2, b2 being POINT of IPP st not p on K & not p on L & a1 on K & b1 on K & (IncProj (K,p,L)) . a1 = a2 & (IncProj (K,p,L)) . b1 = b2 & a2 = b2 holds a1 = b1 proof let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for p being POINT of IPP for K, L being LINE of IPP for a1, b1, a2, b2 being POINT of IPP st not p on K & not p on L & a1 on K & b1 on K & (IncProj (K,p,L)) . a1 = a2 & (IncProj (K,p,L)) . b1 = b2 & a2 = b2 holds a1 = b1 let p be POINT of IPP; ::_thesis: for K, L being LINE of IPP for a1, b1, a2, b2 being POINT of IPP st not p on K & not p on L & a1 on K & b1 on K & (IncProj (K,p,L)) . a1 = a2 & (IncProj (K,p,L)) . b1 = b2 & a2 = b2 holds a1 = b1 let K, L be LINE of IPP; ::_thesis: for a1, b1, a2, b2 being POINT of IPP st not p on K & not p on L & a1 on K & b1 on K & (IncProj (K,p,L)) . a1 = a2 & (IncProj (K,p,L)) . b1 = b2 & a2 = b2 holds a1 = b1 let a1, b1, a2, b2 be POINT of IPP; ::_thesis: ( not p on K & not p on L & a1 on K & b1 on K & (IncProj (K,p,L)) . a1 = a2 & (IncProj (K,p,L)) . b1 = b2 & a2 = b2 implies a1 = b1 ) assume that A1: not p on K and A2: not p on L and A3: a1 on K and A4: b1 on K and A5: (IncProj (K,p,L)) . a1 = a2 and A6: (IncProj (K,p,L)) . b1 = b2 and A7: a2 = b2 ; ::_thesis: a1 = b1 reconsider a2 = (IncProj (K,p,L)) . a1 as POINT of IPP by A5; A8: a2 on L by A1, A2, A3, Th20; then consider A being LINE of IPP such that A9: p on A and A10: a1 on A and A11: a2 on A by A1, A2, A3, Def1; reconsider b2 = (IncProj (K,p,L)) . b1 as Element of the Points of IPP by A6; b2 on L by A1, A2, A4, Th20; then consider B being LINE of IPP such that A12: p on B and A13: b1 on B and A14: b2 on B by A1, A2, A4, Def1; A = B by A2, A5, A6, A7, A8, A9, A11, A12, A14, INCPROJ:def_4; hence a1 = b1 by A1, A3, A4, A9, A10, A13, INCPROJ:def_4; ::_thesis: verum end; theorem Th24: :: PROJRED1:24 for IPP being 2-dimensional Desarguesian IncProjSp for p, x being POINT of IPP for K, L being LINE of IPP st not p on K & not p on L & x on K & x on L holds (IncProj (K,p,L)) . x = x proof let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for p, x being POINT of IPP for K, L being LINE of IPP st not p on K & not p on L & x on K & x on L holds (IncProj (K,p,L)) . x = x let p, x be POINT of IPP; ::_thesis: for K, L being LINE of IPP st not p on K & not p on L & x on K & x on L holds (IncProj (K,p,L)) . x = x let K, L be LINE of IPP; ::_thesis: ( not p on K & not p on L & x on K & x on L implies (IncProj (K,p,L)) . x = x ) A1: ex A being LINE of IPP st ( p on A & x on A ) by INCPROJ:def_5; assume ( not p on K & not p on L & x on K & x on L ) ; ::_thesis: (IncProj (K,p,L)) . x = x hence (IncProj (K,p,L)) . x = x by A1, Def1; ::_thesis: verum end; theorem :: PROJRED1:25 for IPP being 2-dimensional Desarguesian IncProjSp for p, q, c being POINT of IPP for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R & c on K & c on L & c on R & K <> R holds ex o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) proof let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for p, q, c being POINT of IPP for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R & c on K & c on L & c on R & K <> R holds ex o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) let p, q, c be POINT of IPP; ::_thesis: for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R & c on K & c on L & c on R & K <> R holds ex o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) let K, L, R be LINE of IPP; ::_thesis: ( not p on K & not p on L & not q on L & not q on R & c on K & c on L & c on R & K <> R implies ex o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) ) assume that A1: not p on K and A2: not p on L and A3: not q on L and A4: not q on R and A5: c on K and A6: c on L and A7: c on R and A8: K <> R ; ::_thesis: ex o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) defpred S1[ set ] means ex k being POINT of IPP st ( $1 = k & k on K ); consider X being set such that A9: for x being set holds ( x in X iff ( x in the Points of IPP & S1[x] ) ) from XBOOLE_0:sch_1(); A10: ( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= the Points of IPP & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= the Points of IPP ) proof set f = (IncProj (L,q,R)) * (IncProj (K,p,L)); dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22; hence dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= the Points of IPP ; ::_thesis: rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= the Points of IPP rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) by A1, A2, A3, A4, Th22; hence rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= the Points of IPP by RELAT_1:def_19; ::_thesis: verum end; A11: now__::_thesis:_(_p_<>_q_implies_ex_o_being_POINT_of_IPP_st_ (_not_o_on_K_&_not_o_on_R_&_(IncProj_(L,q,R))_*_(IncProj_(K,p,L))_=_IncProj_(K,o,R)_)_) A12: now__::_thesis:_(_L_=_R_implies_ex_p,_o_being_POINT_of_IPP_st_ (_not_o_on_K_&_not_o_on_R_&_(IncProj_(L,q,R))_*_(IncProj_(K,p,L))_=_IncProj_(K,o,R)_)_) A13: X c= dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) ) assume A14: e in X ; ::_thesis: e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) then reconsider e = e as Element of the Points of IPP by A9; A15: ex e9 being POINT of IPP st ( e = e9 & e9 on K ) by A9, A14; dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22; hence e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A1, A2, A15, Def1; ::_thesis: verum end; assume A16: L = R ; ::_thesis: ex p, o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) A17: X c= dom (IncProj (K,p,R)) proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in dom (IncProj (K,p,R)) ) assume A18: e in X ; ::_thesis: e in dom (IncProj (K,p,R)) then reconsider e = e as POINT of IPP by A9; ex e9 being POINT of IPP st ( e = e9 & e9 on K ) by A9, A18; hence e in dom (IncProj (K,p,R)) by A1, A2, A16, Def1; ::_thesis: verum end; A19: for x being POINT of IPP st x in X holds ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x proof let x be Element of the Points of IPP; ::_thesis: ( x in X implies ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x ) assume A20: x in X ; ::_thesis: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x then A21: ((IncProj (R,q,R)) * (IncProj (K,p,R))) . x = (IncProj (R,q,R)) . ((IncProj (K,p,R)) . x) by A16, A13, FUNCT_1:12; A22: x on K by A1, A2, A16, A17, A20, Def1; then reconsider y = (IncProj (K,p,R)) . x as POINT of IPP by A1, A2, A16, Th19; y on R by A1, A2, A16, A22, Th20; hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x by A3, A16, A21, Th18; ::_thesis: verum end; dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= X proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) or e in X ) assume e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) ; ::_thesis: e in X then A23: e in dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22; then reconsider e = e as POINT of IPP ; e on K by A1, A2, A23, Def1; hence e in X by A9; ::_thesis: verum end; then A24: X = dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A13, XBOOLE_0:def_10; A25: (IncProj (L,q,R)) * (IncProj (K,p,L)) is PartFunc of the Points of IPP, the Points of IPP by A10, RELSET_1:4; take p = p; ::_thesis: ex o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) dom (IncProj (K,p,R)) c= X proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom (IncProj (K,p,R)) or e in X ) assume A26: e in dom (IncProj (K,p,R)) ; ::_thesis: e in X then reconsider e = e as POINT of IPP ; e on K by A1, A2, A16, A26, Def1; hence e in X by A9; ::_thesis: verum end; then X = dom (IncProj (K,p,R)) by A17, XBOOLE_0:def_10; hence ex o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) by A1, A2, A16, A24, A19, A25, PARTFUN1:5; ::_thesis: verum end; consider A being LINE of IPP such that A27: p on A and A28: q on A by INCPROJ:def_5; consider c1 being POINT of IPP such that A29: c1 on K and A30: c1 on A by INCPROJ:def_9; reconsider c2 = (IncProj (K,p,L)) . c1 as Element of the Points of IPP by A1, A2, A29, Th19; A31: c2 on L by A1, A2, A29, Th20; then reconsider c3 = (IncProj (L,q,R)) . c2 as POINT of IPP by A3, A4, Th19; A32: c3 on R by A3, A4, A31, Th20; consider a1 being POINT of IPP such that A33: a1 on K and A34: c1 <> a1 and A35: c <> a1 by Th8; reconsider a2 = (IncProj (K,p,L)) . a1 as POINT of IPP by A1, A2, A33, Th19; A36: a2 on L by A1, A2, A33, Th20; then reconsider a3 = (IncProj (L,q,R)) . a2 as POINT of IPP by A3, A4, Th19; A37: a3 on R by A3, A4, A36, Th20; A38: not a3 on K proof assume a3 on K ; ::_thesis: contradiction then A39: c = a3 by A5, A7, A8, A37, INCPROJ:def_4; ex C being LINE of IPP st ( q on C & c on C ) by INCPROJ:def_5; then (IncProj (L,q,R)) . c = a3 by A3, A4, A6, A7, A39, Def1; then A40: c = a2 by A3, A4, A6, A36, Th23; ex D being LINE of IPP st ( p on D & c on D ) by INCPROJ:def_5; then (IncProj (K,p,L)) . c = a2 by A1, A2, A5, A6, A40, Def1; hence contradiction by A1, A2, A5, A33, A35, Th23; ::_thesis: verum end; consider B being LINE of IPP such that A41: ( a1 on B & a3 on B ) by INCPROJ:def_5; consider o being POINT of IPP such that A42: o on A and A43: o on B by INCPROJ:def_9; A44: not a1 on R by A5, A7, A8, A33, A35, INCPROJ:def_4; A45: ( not o on K & not o on R ) proof A46: now__::_thesis:_not_o_on_R assume A47: o on R ; ::_thesis: contradiction then A48: o = a3 by A37, A41, A43, A44, INCPROJ:def_4; consider A2 being LINE of IPP such that A49: q on A2 and A50: c2 on A2 and A51: c3 on A2 by A3, A4, A31, A32, Def1; ex A1 being LINE of IPP st ( p on A1 & c1 on A1 & c2 on A1 ) by A1, A2, A29, A31, Def1; then c2 on A by A1, A27, A29, A30, INCPROJ:def_4; then A = A2 by A3, A28, A31, A49, A50, INCPROJ:def_4; then o = c3 by A4, A42, A32, A47, A49, A51, INCPROJ:def_4; then c2 = a2 by A3, A4, A36, A31, A48, Th23; hence contradiction by A1, A2, A29, A33, A34, Th23; ::_thesis: verum end; A52: now__::_thesis:_not_o_on_K assume A53: o on K ; ::_thesis: contradiction then o = c1 by A1, A27, A29, A30, A42, INCPROJ:def_4; hence contradiction by A33, A34, A41, A43, A38, A53, INCPROJ:def_4; ::_thesis: verum end; assume ( o on K or o on R ) ; ::_thesis: contradiction hence contradiction by A52, A46; ::_thesis: verum end; assume A54: p <> q ; ::_thesis: ex o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) A55: now__::_thesis:_(_L_<>_R_&_K_<>_L_implies_ex_o_being_POINT_of_IPP_st_ (_not_o_on_K_&_not_o_on_R_&_(IncProj_(L,q,R))_*_(IncProj_(K,p,L))_=_IncProj_(K,o,R)_)_) assume that A56: L <> R and K <> L ; ::_thesis: ex o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) A57: X c= dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) ) assume A58: e in X ; ::_thesis: e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) then reconsider e = e as POINT of IPP by A9; A59: ex e9 being POINT of IPP st ( e = e9 & e9 on K ) by A9, A58; dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22; hence e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A1, A2, A59, Def1; ::_thesis: verum end; A60: for x being POINT of IPP st x in X holds ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x proof let x be Element of the Points of IPP; ::_thesis: ( x in X implies ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x ) assume A61: x in X ; ::_thesis: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x A62: now__::_thesis:_(_x_=_c_implies_((IncProj_(L,q,R))_*_(IncProj_(K,p,L)))_._x_=_(IncProj_(K,o,R))_._x_) assume A63: x = c ; ::_thesis: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x then ((IncProj (L,q,R)) * (IncProj (K,p,L))) . c = (IncProj (L,q,R)) . ((IncProj (K,p,L)) . c) by A57, A61, FUNCT_1:12; then ((IncProj (L,q,R)) * (IncProj (K,p,L))) . c = (IncProj (L,q,R)) . c by A1, A2, A5, A6, Th24; then ((IncProj (L,q,R)) * (IncProj (K,p,L))) . c = c by A3, A4, A6, A7, Th24; hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x by A5, A7, A45, A63, Th24; ::_thesis: verum end; A64: now__::_thesis:_(_x_<>_c1_&_x_<>_c_&_x_<>_a1_implies_((IncProj_(L,q,R))_*_(IncProj_(K,p,L)))_._x_=_(IncProj_(K,o,R))_._x_) assume that x <> c1 and A65: x <> c and x <> a1 ; ::_thesis: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x proof A66: a2 <> a3 proof assume a2 = a3 ; ::_thesis: contradiction then A67: (IncProj (K,p,L)) . a1 = c by A6, A7, A36, A37, A56, INCPROJ:def_4; (IncProj (K,p,L)) . c = c by A1, A2, A5, A6, Th24; hence contradiction by A1, A2, A5, A33, A35, A67, Th23; ::_thesis: verum end; A68: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (L,q,R)) . ((IncProj (K,p,L)) . x) by A57, A61, FUNCT_1:12; A69: a2 <> c proof assume A70: a2 = c ; ::_thesis: contradiction (IncProj (K,p,L)) . c = c by A1, A2, A5, A6, Th24; hence contradiction by A1, A2, A5, A33, A35, A70, Th23; ::_thesis: verum end; A71: a3 on R by A3, A4, A36, Th20; A72: dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22; then A73: x on K by A1, A2, A57, A61, Def1; then reconsider y = (IncProj (K,p,L)) . x as POINT of IPP by A1, A2, Th19; A74: y on L by A1, A2, A73, Th20; then reconsider z = (IncProj (L,q,R)) . y as POINT of IPP by A3, A4, Th19; consider B3 being LINE of IPP such that A75: ( p on B3 & x on B3 & y on B3 ) by A1, A2, A73, A74, Def1; x on K by A1, A2, A57, A61, A72, Def1; then A76: c <> y by A1, A5, A65, A75, INCPROJ:def_4; consider A1 being LINE of IPP such that A77: q on A1 and A78: ( a2 on A1 & a3 on A1 ) by A3, A4, A36, A37, Def1; A79: {a2,a3,q} on A1 by A77, A78, INCSP_1:2; A80: z on R by A3, A4, A74, Th20; then consider B1 being LINE of IPP such that A81: ( q on B1 & y on B1 & z on B1 ) by A3, A4, A74, Def1; x on K by A1, A2, A57, A61, A72, Def1; then A82: {x,c,a1} on K by A5, A33, INCSP_1:2; consider A3 being Element of the Lines of IPP such that A83: p on A3 and A84: a1 on A3 and A85: a2 on A3 by A1, A2, A33, A36, Def1; A86: {a2,p,a1} on A3 by A83, A84, A85, INCSP_1:2; A1 <> A3 proof assume A1 = A3 ; ::_thesis: contradiction then A = A3 by A54, A27, A28, A77, A83, INCPROJ:def_4; hence contradiction by A1, A29, A30, A33, A34, A83, A84, INCPROJ:def_4; ::_thesis: verum end; then A87: A1,L,A3 are_mutually_different by A2, A3, A77, A83, ZFMISC_1:def_5; A88: {a2,y,c} on L by A6, A36, A74, INCSP_1:2; A89: {p,y,x} on B3 by A75, INCSP_1:2; z on R by A3, A4, A74, Th20; then A90: {a3,z,c} on R by A7, A71, INCSP_1:2; A91: ( {p,o,q} on A & {a3,o,a1} on B ) by A27, A28, A41, A42, A43, INCSP_1:2; A92: a2 <> p by A1, A2, A33, Th20; {y,z,q} on B1 by A81, INCSP_1:2; then consider O being LINE of IPP such that A93: {o,z,x} on O by A69, A66, A76, A88, A79, A86, A89, A91, A82, A90, A87, A92, Th12; A94: o on O by A93, INCSP_1:2; ( x on O & z on O ) by A93, INCSP_1:2; hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x by A45, A73, A80, A94, A68, Def1; ::_thesis: verum end; hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x ; ::_thesis: verum end; A95: now__::_thesis:_(_x_=_c1_implies_((IncProj_(L,q,R))_*_(IncProj_(K,p,L)))_._x_=_(IncProj_(K,o,R))_._x_) assume A96: x = c1 ; ::_thesis: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x proof A97: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . c1 = c3 by A57, A61, A96, FUNCT_1:12; consider A2 being LINE of IPP such that A98: ( q on A2 & c2 on A2 ) and A99: c3 on A2 by A3, A4, A31, A32, Def1; ex A1 being Element of the Lines of IPP st ( p on A1 & c1 on A1 & c2 on A1 ) by A1, A2, A29, A31, Def1; then c2 on A by A1, A27, A29, A30, INCPROJ:def_4; then A = A2 by A3, A28, A31, A98, INCPROJ:def_4; hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x by A29, A30, A42, A32, A45, A96, A97, A99, Def1; ::_thesis: verum end; hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x ; ::_thesis: verum end; now__::_thesis:_(_x_=_a1_implies_((IncProj_(L,q,R))_*_(IncProj_(K,p,L)))_._x_=_(IncProj_(K,o,R))_._x_) assume A100: x = a1 ; ::_thesis: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x then ((IncProj (L,q,R)) * (IncProj (K,p,L))) . a1 = a3 by A57, A61, FUNCT_1:12; hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x by A33, A37, A41, A43, A45, A100, Def1; ::_thesis: verum end; hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x by A62, A95, A64; ::_thesis: verum end; A101: dom (IncProj (K,o,R)) c= X proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom (IncProj (K,o,R)) or e in X ) assume A102: e in dom (IncProj (K,o,R)) ; ::_thesis: e in X then reconsider e = e as POINT of IPP ; e on K by A45, A102, Def1; hence e in X by A9; ::_thesis: verum end; X c= dom (IncProj (K,o,R)) proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in dom (IncProj (K,o,R)) ) assume A103: e in X ; ::_thesis: e in dom (IncProj (K,o,R)) then reconsider e = e as POINT of IPP by A9; ex e9 being POINT of IPP st ( e = e9 & e9 on K ) by A9, A103; hence e in dom (IncProj (K,o,R)) by A45, Def1; ::_thesis: verum end; then A104: X = dom (IncProj (K,o,R)) by A101, XBOOLE_0:def_10; A105: (IncProj (L,q,R)) * (IncProj (K,p,L)) is PartFunc of the Points of IPP, the Points of IPP by A10, RELSET_1:4; dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= X proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) or e in X ) assume e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) ; ::_thesis: e in X then A106: e in dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22; then reconsider e = e as POINT of IPP ; e on K by A1, A2, A106, Def1; hence e in X by A9; ::_thesis: verum end; then X = dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A57, XBOOLE_0:def_10; hence ex o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) by A45, A60, A104, A105, PARTFUN1:5; ::_thesis: verum end; now__::_thesis:_(_K_=_L_implies_ex_q,_o_being_POINT_of_IPP_st_ (_not_o_on_K_&_not_o_on_R_&_(IncProj_(L,q,R))_*_(IncProj_(K,p,L))_=_IncProj_(K,o,R)_)_) A107: X c= dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) ) assume A108: e in X ; ::_thesis: e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) then reconsider e = e as Element of the Points of IPP by A9; A109: ex e9 being POINT of IPP st ( e = e9 & e9 on K ) by A9, A108; dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22; hence e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A1, A2, A109, Def1; ::_thesis: verum end; dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= X proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) or e in X ) assume e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) ; ::_thesis: e in X then A110: e in dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22; then reconsider e = e as POINT of IPP ; e on K by A1, A2, A110, Def1; hence e in X by A9; ::_thesis: verum end; then A111: X = dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A107, XBOOLE_0:def_10; A112: (IncProj (L,q,R)) * (IncProj (K,p,L)) is PartFunc of the Points of IPP, the Points of IPP by A10, RELSET_1:4; assume A113: K = L ; ::_thesis: ex q, o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) A114: X c= dom (IncProj (K,q,R)) proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in dom (IncProj (K,q,R)) ) assume A115: e in X ; ::_thesis: e in dom (IncProj (K,q,R)) then reconsider e = e as POINT of IPP by A9; ex e9 being POINT of IPP st ( e = e9 & e9 on K ) by A9, A115; hence e in dom (IncProj (K,q,R)) by A3, A4, A113, Def1; ::_thesis: verum end; A116: for x being POINT of IPP st x in X holds ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,q,R)) . x proof let x be Element of the Points of IPP; ::_thesis: ( x in X implies ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,q,R)) . x ) assume x in X ; ::_thesis: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,q,R)) . x then ( x on K & ((IncProj (K,q,R)) * (IncProj (K,p,K))) . x = (IncProj (K,q,R)) . ((IncProj (K,p,K)) . x) ) by A3, A4, A113, A107, A114, Def1, FUNCT_1:12; hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,q,R)) . x by A1, A113, Th18; ::_thesis: verum end; take q = q; ::_thesis: ex o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) dom (IncProj (K,q,R)) c= X proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom (IncProj (K,q,R)) or e in X ) assume A117: e in dom (IncProj (K,q,R)) ; ::_thesis: e in X then reconsider e = e as POINT of IPP ; e on K by A3, A4, A113, A117, Def1; hence e in X by A9; ::_thesis: verum end; then X = dom (IncProj (K,q,R)) by A114, XBOOLE_0:def_10; hence ex o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) by A3, A4, A113, A111, A116, A112, PARTFUN1:5; ::_thesis: verum end; hence ex o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) by A12, A55; ::_thesis: verum end; now__::_thesis:_(_p_=_q_implies_ex_o_being_POINT_of_IPP_st_ (_not_o_on_K_&_not_o_on_R_&_(IncProj_(L,q,R))_*_(IncProj_(K,p,L))_=_IncProj_(K,o,R)_)_) A118: X c= dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) ) assume A119: e in X ; ::_thesis: e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) then reconsider e = e as POINT of IPP by A9; A120: ex e9 being Element of the Points of IPP st ( e = e9 & e9 on K ) by A9, A119; dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22; hence e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A1, A2, A120, Def1; ::_thesis: verum end; assume A121: p = q ; ::_thesis: ex o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) A122: X c= dom (IncProj (K,p,R)) proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in dom (IncProj (K,p,R)) ) assume A123: e in X ; ::_thesis: e in dom (IncProj (K,p,R)) then reconsider e = e as POINT of IPP by A9; ex e9 being POINT of IPP st ( e = e9 & e9 on K ) by A9, A123; hence e in dom (IncProj (K,p,R)) by A1, A4, A121, Def1; ::_thesis: verum end; A124: for x being POINT of IPP st x in X holds ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x proof let x be POINT of IPP; ::_thesis: ( x in X implies ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x ) assume A125: x in X ; ::_thesis: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x then A126: ((IncProj (L,p,R)) * (IncProj (K,p,L))) . x = (IncProj (L,p,R)) . ((IncProj (K,p,L)) . x) by A121, A118, FUNCT_1:12; A127: x on K by A1, A4, A121, A122, A125, Def1; then reconsider y = (IncProj (K,p,L)) . x as POINT of IPP by A1, A2, Th19; A128: y on L by A1, A2, A127, Th20; then reconsider z = (IncProj (L,p,R)) . y as POINT of IPP by A2, A4, A121, Th19; consider A being LINE of IPP such that A129: ( p on A & y on A ) by INCPROJ:def_5; A130: z on R by A2, A4, A121, A128, Th20; then consider C being LINE of IPP such that A131: ( p on C & y on C ) and A132: z on C by A2, A4, A121, A128, Def1; A133: A = C by A2, A128, A129, A131, INCPROJ:def_4; consider B being LINE of IPP such that A134: p on B and A135: x on B and A136: y on B by A1, A2, A127, A128, Def1; A = B by A2, A128, A129, A134, A136, INCPROJ:def_4; hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x by A1, A4, A121, A127, A126, A134, A135, A130, A132, A133, Def1; ::_thesis: verum end; dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= X proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) or e in X ) assume e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) ; ::_thesis: e in X then A137: e in dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22; then reconsider e = e as POINT of IPP ; e on K by A1, A2, A137, Def1; hence e in X by A9; ::_thesis: verum end; then A138: X = dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A118, XBOOLE_0:def_10; A139: (IncProj (L,q,R)) * (IncProj (K,p,L)) is PartFunc of the Points of IPP, the Points of IPP by A10, RELSET_1:4; dom (IncProj (K,p,R)) c= X proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom (IncProj (K,p,R)) or e in X ) assume A140: e in dom (IncProj (K,p,R)) ; ::_thesis: e in X then reconsider e = e as POINT of IPP ; e on K by A1, A4, A121, A140, Def1; hence e in X by A9; ::_thesis: verum end; then X = dom (IncProj (K,p,R)) by A122, XBOOLE_0:def_10; hence ex o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) by A1, A4, A121, A138, A124, A139, PARTFUN1:5; ::_thesis: verum end; hence ex o being POINT of IPP st ( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) by A11; ::_thesis: verum end;