:: PARDEPAP semantic presentation begin theorem Th1: :: PARDEPAP:1 for SAS being AffinPlane st SAS is Pappian holds for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds a3,b1 // a1,b3 proof let SAS be AffinPlane; ::_thesis: ( SAS is Pappian implies for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds a3,b1 // a1,b3 ) assume A1: SAS is Pappian ; ::_thesis: for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds a3,b1 // a1,b3 let a1, a2, a3, b1, b2, b3 be Element of SAS; ::_thesis: ( a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 implies a3,b1 // a1,b3 ) assume that A2: a1,a2 // a1,a3 and A3: b1,b2 // b1,b3 and A4: a1,b2 // a2,b1 and A5: a2,b3 // a3,b2 ; ::_thesis: a3,b1 // a1,b3 LIN a1,a2,a3 by A2, AFF_1:def_1; then consider M being Subset of SAS such that A6: M is being_line and A7: a1 in M and A8: a2 in M and A9: a3 in M by AFF_1:21; LIN b1,b2,b3 by A3, AFF_1:def_1; then consider N being Subset of SAS such that A10: N is being_line and A11: b1 in N and A12: b2 in N and A13: b3 in N by AFF_1:21; A14: now__::_thesis:_(_M_<>_N_&_not_M_//_N_implies_a3,b1_//_a1,b3_) assume that A15: M <> N and A16: not M // N ; ::_thesis: a3,b1 // a1,b3 consider o being Element of SAS such that A17: o in M and A18: o in N by A6, A10, A16, AFF_1:58; A19: now__::_thesis:_(_o_<>_a1_&_b1_<>_o_&_o_=_b3_implies_a3,b1_//_a1,b3_) assume that A20: o <> a1 and A21: b1 <> o and A22: o = b3 ; ::_thesis: a3,b1 // a1,b3 A23: now__::_thesis:_(_a2_<>_o_implies_a3,b1_//_a1,b3_) assume a2 <> o ; ::_thesis: a3,b1 // a1,b3 then b2 in M by A5, A6, A8, A9, A17, A22, AFF_1:48; then b2 = o by A6, A10, A12, A15, A17, A18, AFF_1:18; then b1 in M by A4, A6, A7, A8, A17, A20, AFF_1:48; hence a3,b1 // a1,b3 by A6, A7, A9, A17, A22, AFF_1:51; ::_thesis: verum end; now__::_thesis:_(_a2_=_o_implies_a3,b1_//_a1,b3_) assume a2 = o ; ::_thesis: a3,b1 // a1,b3 then o,b1 // b2,a1 by A4, AFF_1:4; then a1 in N by A10, A11, A12, A13, A21, A22, AFF_1:48; hence a3,b1 // a1,b3 by A6, A7, A10, A15, A17, A18, A20, AFF_1:18; ::_thesis: verum end; hence a3,b1 // a1,b3 by A23; ::_thesis: verum end; A24: now__::_thesis:_(_o_<>_a1_&_b1_=_o_implies_a3,b1_//_a1,b3_) assume that o <> a1 and A25: b1 = o ; ::_thesis: a3,b1 // a1,b3 A26: o,a2 // a1,b2 by A4, A25, AFF_1:4; A27: now__::_thesis:_(_a2_<>_o_implies_a3,b1_//_a1,b3_) assume a2 <> o ; ::_thesis: a3,b1 // a1,b3 then b2 in M by A6, A7, A8, A17, A26, AFF_1:48; then b2 = o by A6, A10, A12, A15, A17, A18, AFF_1:18; then A28: o,a3 // a2,b3 by A5, AFF_1:4; now__::_thesis:_(_o_<>_a3_implies_a3,b1_//_a1,b3_) assume o <> a3 ; ::_thesis: a3,b1 // a1,b3 then b3 in M by A6, A8, A9, A17, A28, AFF_1:48; hence a3,b1 // a1,b3 by A6, A7, A9, A17, A25, AFF_1:51; ::_thesis: verum end; hence a3,b1 // a1,b3 by A25, AFF_1:3; ::_thesis: verum end; now__::_thesis:_(_a2_=_o_implies_a3,b1_//_a1,b3_) assume A29: a2 = o ; ::_thesis: a3,b1 // a1,b3 now__::_thesis:_(_b3_<>_o_implies_a3,b1_//_a1,b3_) assume A30: b3 <> o ; ::_thesis: a3,b1 // a1,b3 o,b3 // b2,a3 by A5, A29, AFF_1:4; then a3 in N by A10, A12, A13, A18, A30, AFF_1:48; then b1 = a3 by A6, A9, A10, A15, A17, A18, A25, AFF_1:18; hence a3,b1 // a1,b3 by AFF_1:3; ::_thesis: verum end; hence a3,b1 // a1,b3 by A6, A7, A9, A17, A25, AFF_1:51; ::_thesis: verum end; hence a3,b1 // a1,b3 by A27; ::_thesis: verum end; A31: now__::_thesis:_(_o_=_a1_implies_a3,b1_//_a1,b3_) assume A32: o = a1 ; ::_thesis: a3,b1 // a1,b3 then A33: o,b2 // b1,a2 by A4, AFF_1:4; A34: now__::_thesis:_(_b2_<>_o_implies_a3,b1_//_a1,b3_) assume b2 <> o ; ::_thesis: a3,b1 // a1,b3 then a2 in N by A10, A11, A12, A18, A33, AFF_1:48; then a2 = o by A6, A8, A10, A15, A17, A18, AFF_1:18; then A35: o,b3 // b2,a3 by A5, AFF_1:4; now__::_thesis:_(_o_<>_b3_implies_a3,b1_//_a1,b3_) assume o <> b3 ; ::_thesis: a3,b1 // a1,b3 then a3 in N by A10, A12, A13, A18, A35, AFF_1:48; hence a3,b1 // a1,b3 by A10, A11, A13, A18, A32, AFF_1:51; ::_thesis: verum end; hence a3,b1 // a1,b3 by A32, AFF_1:3; ::_thesis: verum end; now__::_thesis:_(_b2_=_o_implies_a3,b1_//_a1,b3_) assume A36: b2 = o ; ::_thesis: a3,b1 // a1,b3 now__::_thesis:_(_a3_<>_o_implies_a3,b1_//_a1,b3_) assume A37: a3 <> o ; ::_thesis: a3,b1 // a1,b3 o,a3 // a2,b3 by A5, A36, AFF_1:4; then b3 in M by A6, A8, A9, A17, A37, AFF_1:48; then a1 = b3 by A6, A10, A13, A15, A17, A18, A32, AFF_1:18; hence a3,b1 // a1,b3 by AFF_1:3; ::_thesis: verum end; hence a3,b1 // a1,b3 by A10, A11, A13, A18, A32, AFF_1:51; ::_thesis: verum end; hence a3,b1 // a1,b3 by A34; ::_thesis: verum end; A38: now__::_thesis:_(_o_<>_a1_&_b1_<>_o_&_o_<>_b3_&_o_=_a3_implies_a3,b1_//_a1,b3_) assume that A39: o <> a1 and A40: b1 <> o and o <> b3 and A41: o = a3 ; ::_thesis: a3,b1 // a1,b3 A42: o,b2 // b3,a2 by A5, A41, AFF_1:4; A43: now__::_thesis:_(_b2_<>_o_implies_a3,b1_//_a1,b3_) assume b2 <> o ; ::_thesis: a3,b1 // a1,b3 then a2 in N by A10, A12, A13, A18, A42, AFF_1:48; then a2 = o by A6, A8, A10, A15, A17, A18, AFF_1:18; then o,b1 // b2,a1 by A4, AFF_1:4; then a1 in N by A10, A11, A12, A18, A40, AFF_1:48; hence a3,b1 // a1,b3 by A10, A11, A13, A18, A41, AFF_1:51; ::_thesis: verum end; now__::_thesis:_(_b2_=_o_implies_a3,b1_//_a1,b3_) assume b2 = o ; ::_thesis: a3,b1 // a1,b3 then b1 in M by A4, A6, A7, A8, A9, A39, A41, AFF_1:48; hence a3,b1 // a1,b3 by A6, A10, A11, A15, A17, A18, A40, AFF_1:18; ::_thesis: verum end; hence a3,b1 // a1,b3 by A43; ::_thesis: verum end; now__::_thesis:_(_o_<>_a1_&_o_<>_b1_&_o_<>_b3_&_o_<>_a3_implies_a3,b1_//_a1,b3_) assume that A44: ( o <> a1 & o <> b1 ) and A45: o <> b3 and A46: o <> a3 ; ::_thesis: a3,b1 // a1,b3 A47: o <> b2 proof assume o = b2 ; ::_thesis: contradiction then o,a3 // a2,b3 by A5, AFF_1:4; then b3 in M by A6, A8, A9, A17, A46, AFF_1:48; hence contradiction by A6, A10, A13, A15, A17, A18, A45, AFF_1:18; ::_thesis: verum end; o <> a2 proof assume o = a2 ; ::_thesis: contradiction then o,b3 // b2,a3 by A5, AFF_1:4; then a3 in N by A10, A12, A13, A18, A45, AFF_1:48; hence contradiction by A6, A9, A10, A15, A17, A18, A46, AFF_1:18; ::_thesis: verum end; then a1,b3 // a3,b1 by A1, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A15, A17, A18, A44, A45, A46, A47, AFF_2:def_2; hence a3,b1 // a1,b3 by AFF_1:4; ::_thesis: verum end; hence a3,b1 // a1,b3 by A31, A24, A19, A38; ::_thesis: verum end; A48: SAS is satisfying_pap by A1, AFF_2:9; now__::_thesis:_(_M_<>_N_&_M_//_N_implies_a3,b1_//_a1,b3_) assume ( M <> N & M // N ) ; ::_thesis: a3,b1 // a1,b3 then a1,b3 // a3,b1 by A48, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, AFF_2:def_13; hence a3,b1 // a1,b3 by AFF_1:4; ::_thesis: verum end; hence a3,b1 // a1,b3 by A6, A7, A9, A11, A13, A14, AFF_1:51; ::_thesis: verum end; theorem Th2: :: PARDEPAP:2 for SAS being AffinPlane st SAS is Desarguesian holds for o, a, a9, b, b9, c, c9 being Element of SAS st not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 proof let SAS be AffinPlane; ::_thesis: ( SAS is Desarguesian implies for o, a, a9, b, b9, c, c9 being Element of SAS st not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) assume A1: SAS is Desarguesian ; ::_thesis: for o, a, a9, b, b9, c, c9 being Element of SAS st not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 let o, a, a9, b, b9, c, c9 be Element of SAS; ::_thesis: ( not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 ) assume that A2: not o,a // o,b and A3: not o,a // o,c and A4: o,a // o,a9 and A5: o,b // o,b9 and A6: o,c // o,c9 and A7: ( a,b // a9,b9 & a,c // a9,c9 ) ; ::_thesis: b,c // b9,c9 A8: ( o <> a & o <> b ) by A2, AFF_1:3; A9: o <> c by A3, AFF_1:3; LIN o,b,b9 by A5, AFF_1:def_1; then consider P being Subset of SAS such that A10: ( P is being_line & o in P ) and A11: b in P and A12: b9 in P by AFF_1:21; LIN o,a,a9 by A4, AFF_1:def_1; then consider A being Subset of SAS such that A13: ( A is being_line & o in A & a in A ) and A14: a9 in A by AFF_1:21; LIN o,c,c9 by A6, AFF_1:def_1; then consider C being Subset of SAS such that A15: ( C is being_line & o in C ) and A16: c in C and A17: c9 in C by AFF_1:21; A18: A <> C by A3, A13, A16, AFF_1:51; A <> P by A2, A13, A11, AFF_1:51; hence b,c // b9,c9 by A1, A7, A13, A14, A10, A11, A12, A15, A16, A17, A8, A9, A18, AFF_2:def_4; ::_thesis: verum end; theorem Th3: :: PARDEPAP:3 for SAS being AffinPlane st SAS is translational holds for a, a9, b, b9, c, c9 being Element of SAS st not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 proof let SAS be AffinPlane; ::_thesis: ( SAS is translational implies for a, a9, b, b9, c, c9 being Element of SAS st not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) assume A1: SAS is translational ; ::_thesis: for a, a9, b, b9, c, c9 being Element of SAS st not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 let a, a9, b, b9, c, c9 be Element of SAS; ::_thesis: ( not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 ) assume that A2: not a,a9 // a,b and A3: not a,a9 // a,c and A4: a,a9 // b,b9 and A5: a,a9 // c,c9 and A6: ( a,b // a9,b9 & a,c // a9,c9 ) ; ::_thesis: b,c // b9,c9 set A = Line (a,a9); A7: a <> a9 by A2, AFF_1:3; then A8: Line (a,a9) is being_line by AFF_1:def_3; then consider C being Subset of SAS such that A9: c in C and A10: Line (a,a9) // C by AFF_1:49; A11: C is being_line by A10, AFF_1:36; A12: ( a in Line (a,a9) & a9 in Line (a,a9) ) by AFF_1:15; then A13: Line (a,a9) <> C by A3, A8, A9, AFF_1:51; A14: a,a9 // Line (a,a9) by A8, A12, AFF_1:23; then a,a9 // C by A10, AFF_1:43; then c,c9 // C by A5, A7, AFF_1:32; then A15: c9 in C by A9, A11, AFF_1:23; consider P being Subset of SAS such that A16: b in P and A17: Line (a,a9) // P by A8, AFF_1:49; A18: P is being_line by A17, AFF_1:36; a,a9 // P by A14, A17, AFF_1:43; then b,b9 // P by A4, A7, AFF_1:32; then A19: b9 in P by A16, A18, AFF_1:23; Line (a,a9) <> P by A2, A8, A12, A16, AFF_1:51; hence b,c // b9,c9 by A1, A6, A8, A12, A16, A17, A9, A10, A18, A11, A19, A15, A13, AFF_2:def_11; ::_thesis: verum end; theorem :: PARDEPAP:4 ex SAS being AffinPlane st ( ( for o, a, a9, b, b9, c, c9 being Element of SAS st not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) & ( for a, a9, b, b9, c, c9 being Element of SAS st not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) & ( for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds a3,b1 // a1,b3 ) & ( for a, b, c, d being Element of SAS st not a,b // a,c & a,b // c,d & a,c // b,d holds not a,d // b,c ) ) proof set PAS = the Pappian Desarguesian translational Fanoian AffinPlane; reconsider SAS = the Pappian Desarguesian translational Fanoian AffinPlane as AffinPlane ; take SAS ; ::_thesis: ( ( for o, a, a9, b, b9, c, c9 being Element of SAS st not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) & ( for a, a9, b, b9, c, c9 being Element of SAS st not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) & ( for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds a3,b1 // a1,b3 ) & ( for a, b, c, d being Element of SAS st not a,b // a,c & a,b // c,d & a,c // b,d holds not a,d // b,c ) ) thus ( ( for o, a, a9, b, b9, c, c9 being Element of SAS st not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) & ( for a, a9, b, b9, c, c9 being Element of SAS st not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) & ( for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds a3,b1 // a1,b3 ) & ( for a, b, c, d being Element of SAS st not a,b // a,c & a,b // c,d & a,c // b,d holds not a,d // b,c ) ) by Th1, Th2, Th3, PAPDESAF:def_1; ::_thesis: verum end; theorem :: PARDEPAP:5 for SAS being AffinPlane for o, a being Element of SAS ex p being Element of SAS st for b, c being Element of SAS holds ( o,a // o,p & ex d being Element of SAS st ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) proof let SAS be AffinPlane; ::_thesis: for o, a being Element of SAS ex p being Element of SAS st for b, c being Element of SAS holds ( o,a // o,p & ex d being Element of SAS st ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) let o, a be Element of SAS; ::_thesis: ex p being Element of SAS st for b, c being Element of SAS holds ( o,a // o,p & ex d being Element of SAS st ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) ex p being Element of SAS st ( o <> p & o,a // o,p ) proof consider x, y being Element of SAS such that A1: x <> y by DIRAF:40; now__::_thesis:_(_a_=_o_implies_ex_p_being_Element_of_SAS_st_ (_o_<>_p_&_o,a_//_o,p_)_) assume a = o ; ::_thesis: ex p being Element of SAS st ( o <> p & o,a // o,p ) then A2: ( o,a // o,x & o,a // o,y ) by AFF_1:3; ( o <> x or o <> y ) by A1; hence ex p being Element of SAS st ( o <> p & o,a // o,p ) by A2; ::_thesis: verum end; hence ex p being Element of SAS st ( o <> p & o,a // o,p ) by AFF_1:2; ::_thesis: verum end; then consider p being Element of SAS such that A3: o <> p and A4: o,a // o,p ; take p ; ::_thesis: for b, c being Element of SAS holds ( o,a // o,p & ex d being Element of SAS st ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) thus for b, c being Element of SAS holds ( o,a // o,p & ex d being Element of SAS st ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) ::_thesis: verum proof let b, c be Element of SAS; ::_thesis: ( o,a // o,p & ex d being Element of SAS st ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) ex d being Element of SAS st ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) proof now__::_thesis:_(_o,p_//_o,b_implies_ex_d_being_Element_of_SAS_st_ (_o,p_//_o,b_implies_(_o,c_//_o,d_&_p,c_//_b,d_)_)_) assume o,p // o,b ; ::_thesis: ex d being Element of SAS st ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) then p,o // o,b by AFF_1:4; then consider d being Element of SAS such that A5: ( c,o // o,d & c,p // b,d ) by A3, DIRAF:40; ( o,c // o,d & p,c // b,d ) by A5, AFF_1:4; hence ex d being Element of SAS st ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ; ::_thesis: verum end; hence ex d being Element of SAS st ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ; ::_thesis: verum end; hence ( o,a // o,p & ex d being Element of SAS st ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) by A4; ::_thesis: verum end; end;