:: CONMETR1 semantic presentation begin definition let X be AffinPlane; attrX is satisfying_minor_Scherungssatz means :Def1: :: CONMETR1:def 1 for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X st M // N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4; end; :: deftheorem Def1 defines satisfying_minor_Scherungssatz CONMETR1:def_1_:_ for X being AffinPlane holds ( X is satisfying_minor_Scherungssatz iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X st M // N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 ); definition let X be AffinPlane; attrX is satisfying_major_Scherungssatz means :Def2: :: CONMETR1:def 2 for o, a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X st M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4; end; :: deftheorem Def2 defines satisfying_major_Scherungssatz CONMETR1:def_2_:_ for X being AffinPlane holds ( X is satisfying_major_Scherungssatz iff for o, a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X st M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 ); definition let X be AffinPlane; attrX is satisfying_Scherungssatz means :Def3: :: CONMETR1:def 3 for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X st M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4; end; :: deftheorem Def3 defines satisfying_Scherungssatz CONMETR1:def_3_:_ for X being AffinPlane holds ( X is satisfying_Scherungssatz iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X st M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 ); definition let X be AffinPlane; attrX is satisfying_indirect_Scherungssatz means :Def4: :: CONMETR1:def 4 for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X st M is being_line & N is being_line & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4; end; :: deftheorem Def4 defines satisfying_indirect_Scherungssatz CONMETR1:def_4_:_ for X being AffinPlane holds ( X is satisfying_indirect_Scherungssatz iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X st M is being_line & N is being_line & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 ); definition let X be AffinPlane; attrX is satisfying_minor_indirect_Scherungssatz means :Def5: :: CONMETR1:def 5 for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X st M // N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4; end; :: deftheorem Def5 defines satisfying_minor_indirect_Scherungssatz CONMETR1:def_5_:_ for X being AffinPlane holds ( X is satisfying_minor_indirect_Scherungssatz iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X st M // N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 ); definition let X be AffinPlane; attrX is satisfying_major_indirect_Scherungssatz means :Def6: :: CONMETR1:def 6 for o, a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X st M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4; end; :: deftheorem Def6 defines satisfying_major_indirect_Scherungssatz CONMETR1:def_6_:_ for X being AffinPlane holds ( X is satisfying_major_indirect_Scherungssatz iff for o, a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X st M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 ); theorem Th1: :: CONMETR1:1 for X being AffinPlane holds ( X is satisfying_indirect_Scherungssatz iff ( X is satisfying_minor_indirect_Scherungssatz & X is satisfying_major_indirect_Scherungssatz ) ) proof let X be AffinPlane; ::_thesis: ( X is satisfying_indirect_Scherungssatz iff ( X is satisfying_minor_indirect_Scherungssatz & X is satisfying_major_indirect_Scherungssatz ) ) A1: ( X is satisfying_indirect_Scherungssatz implies X is satisfying_minor_indirect_Scherungssatz ) proof assume A2: X is satisfying_indirect_Scherungssatz ; ::_thesis: X is satisfying_minor_indirect_Scherungssatz now__::_thesis:_for_a1,_a2,_a3,_a4,_b1,_b2,_b3,_b4_being_Element_of_X for_M,_N_being_Subset_of_X_st_M_//_N_&_a1_in_M_&_a3_in_M_&_b2_in_M_&_b4_in_M_&_a2_in_N_&_a4_in_N_&_b1_in_N_&_b3_in_N_&_not_a4_in_M_&_not_a2_in_M_&_not_b1_in_M_&_not_b3_in_M_&_not_a1_in_N_&_not_a3_in_N_&_not_b2_in_N_&_not_b4_in_N_&_a3,a2_//_b3,b2_&_a2,a1_//_b2,b1_&_a1,a4_//_b1,b4_holds_ a3,a4_//_b3,b4 let a1, a2, a3, a4, b1, b2, b3, b4 be Element of X; ::_thesis: for M, N being Subset of X st M // N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 let M, N be Subset of X; ::_thesis: ( M // N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 ) assume that A3: M // N and A4: a1 in M and A5: a3 in M and A6: b2 in M and A7: b4 in M and A8: a2 in N and A9: a4 in N and A10: b1 in N and A11: b3 in N and A12: not a4 in M and A13: not a2 in M and A14: not b1 in M and A15: not b3 in M and A16: not a1 in N and A17: not a3 in N and A18: not b2 in N and A19: not b4 in N and A20: a3,a2 // b3,b2 and A21: a2,a1 // b2,b1 and A22: a1,a4 // b1,b4 ; ::_thesis: a3,a4 // b3,b4 A23: N is being_line by A3, AFF_1:36; M is being_line by A3, AFF_1:36; hence a3,a4 // b3,b4 by A2, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, A23, Def4; ::_thesis: verum end; hence X is satisfying_minor_indirect_Scherungssatz by Def5; ::_thesis: verum end; A24: ( X is satisfying_minor_indirect_Scherungssatz & X is satisfying_major_indirect_Scherungssatz implies X is satisfying_indirect_Scherungssatz ) proof assume that A25: X is satisfying_minor_indirect_Scherungssatz and A26: X is satisfying_major_indirect_Scherungssatz ; ::_thesis: X is satisfying_indirect_Scherungssatz now__::_thesis:_for_a1,_a2,_a3,_a4,_b1,_b2,_b3,_b4_being_Element_of_X for_M,_N_being_Subset_of_X_st_M_is_being_line_&_N_is_being_line_&_a1_in_M_&_a3_in_M_&_b2_in_M_&_b4_in_M_&_a2_in_N_&_a4_in_N_&_b1_in_N_&_b3_in_N_&_not_a4_in_M_&_not_a2_in_M_&_not_b1_in_M_&_not_b3_in_M_&_not_a1_in_N_&_not_a3_in_N_&_not_b2_in_N_&_not_b4_in_N_&_a3,a2_//_b3,b2_&_a2,a1_//_b2,b1_&_a1,a4_//_b1,b4_holds_ a3,a4_//_b3,b4 let a1, a2, a3, a4, b1, b2, b3, b4 be Element of X; ::_thesis: for M, N being Subset of X st M is being_line & N is being_line & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 let M, N be Subset of X; ::_thesis: ( M is being_line & N is being_line & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 ) assume that A27: M is being_line and A28: N is being_line and A29: a1 in M and A30: a3 in M and A31: b2 in M and A32: b4 in M and A33: a2 in N and A34: a4 in N and A35: b1 in N and A36: b3 in N and A37: not a4 in M and A38: not a2 in M and A39: not b1 in M and A40: not b3 in M and A41: not a1 in N and A42: not a3 in N and A43: not b2 in N and A44: not b4 in N and A45: a3,a2 // b3,b2 and A46: a2,a1 // b2,b1 and A47: a1,a4 // b1,b4 ; ::_thesis: a3,a4 // b3,b4 now__::_thesis:_(_not_M_//_N_implies_a3,a4_//_b3,b4_) assume not M // N ; ::_thesis: a3,a4 // b3,b4 then ex o being Element of X st ( o in M & o in N ) by A27, A28, AFF_1:58; hence a3,a4 // b3,b4 by A26, A27, A28, A29, A30, A31, A32, A33, A34, A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A45, A46, A47, Def6; ::_thesis: verum end; hence a3,a4 // b3,b4 by A25, A29, A30, A31, A32, A33, A34, A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A45, A46, A47, Def5; ::_thesis: verum end; hence X is satisfying_indirect_Scherungssatz by Def4; ::_thesis: verum end; ( X is satisfying_indirect_Scherungssatz implies X is satisfying_major_indirect_Scherungssatz ) proof assume X is satisfying_indirect_Scherungssatz ; ::_thesis: X is satisfying_major_indirect_Scherungssatz then for o, a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X st M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 by Def4; hence X is satisfying_major_indirect_Scherungssatz by Def6; ::_thesis: verum end; hence ( X is satisfying_indirect_Scherungssatz iff ( X is satisfying_minor_indirect_Scherungssatz & X is satisfying_major_indirect_Scherungssatz ) ) by A1, A24; ::_thesis: verum end; theorem Th2: :: CONMETR1:2 for X being AffinPlane holds ( X is satisfying_Scherungssatz iff ( X is satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz ) ) proof let X be AffinPlane; ::_thesis: ( X is satisfying_Scherungssatz iff ( X is satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz ) ) A1: ( X is satisfying_Scherungssatz implies X is satisfying_minor_Scherungssatz ) proof assume A2: X is satisfying_Scherungssatz ; ::_thesis: X is satisfying_minor_Scherungssatz now__::_thesis:_for_a1,_a2,_a3,_a4,_b1,_b2,_b3,_b4_being_Element_of_X for_M,_N_being_Subset_of_X_st_M_//_N_&_a1_in_M_&_a3_in_M_&_b1_in_M_&_b3_in_M_&_a2_in_N_&_a4_in_N_&_b2_in_N_&_b4_in_N_&_not_a4_in_M_&_not_a2_in_M_&_not_b2_in_M_&_not_b4_in_M_&_not_a1_in_N_&_not_a3_in_N_&_not_b1_in_N_&_not_b3_in_N_&_a3,a2_//_b3,b2_&_a2,a1_//_b2,b1_&_a1,a4_//_b1,b4_holds_ a3,a4_//_b3,b4 let a1, a2, a3, a4, b1, b2, b3, b4 be Element of X; ::_thesis: for M, N being Subset of X st M // N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 let M, N be Subset of X; ::_thesis: ( M // N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 ) assume that A3: M // N and A4: a1 in M and A5: a3 in M and A6: b1 in M and A7: b3 in M and A8: a2 in N and A9: a4 in N and A10: b2 in N and A11: b4 in N and A12: not a4 in M and A13: not a2 in M and A14: not b2 in M and A15: not b4 in M and A16: not a1 in N and A17: not a3 in N and A18: not b1 in N and A19: not b3 in N and A20: a3,a2 // b3,b2 and A21: a2,a1 // b2,b1 and A22: a1,a4 // b1,b4 ; ::_thesis: a3,a4 // b3,b4 A23: N is being_line by A3, AFF_1:36; M is being_line by A3, AFF_1:36; hence a3,a4 // b3,b4 by A2, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, A23, Def3; ::_thesis: verum end; hence X is satisfying_minor_Scherungssatz by Def1; ::_thesis: verum end; A24: ( X is satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz implies X is satisfying_Scherungssatz ) proof assume that A25: X is satisfying_minor_Scherungssatz and A26: X is satisfying_major_Scherungssatz ; ::_thesis: X is satisfying_Scherungssatz now__::_thesis:_for_a1,_a2,_a3,_a4,_b1,_b2,_b3,_b4_being_Element_of_X for_M,_N_being_Subset_of_X_st_M_is_being_line_&_N_is_being_line_&_a1_in_M_&_a3_in_M_&_b1_in_M_&_b3_in_M_&_a2_in_N_&_a4_in_N_&_b2_in_N_&_b4_in_N_&_not_a4_in_M_&_not_a2_in_M_&_not_b2_in_M_&_not_b4_in_M_&_not_a1_in_N_&_not_a3_in_N_&_not_b1_in_N_&_not_b3_in_N_&_a3,a2_//_b3,b2_&_a2,a1_//_b2,b1_&_a1,a4_//_b1,b4_holds_ a3,a4_//_b3,b4 let a1, a2, a3, a4, b1, b2, b3, b4 be Element of X; ::_thesis: for M, N being Subset of X st M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 let M, N be Subset of X; ::_thesis: ( M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 ) assume that A27: M is being_line and A28: N is being_line and A29: a1 in M and A30: a3 in M and A31: b1 in M and A32: b3 in M and A33: a2 in N and A34: a4 in N and A35: b2 in N and A36: b4 in N and A37: not a4 in M and A38: not a2 in M and A39: not b2 in M and A40: not b4 in M and A41: not a1 in N and A42: not a3 in N and A43: not b1 in N and A44: not b3 in N and A45: a3,a2 // b3,b2 and A46: a2,a1 // b2,b1 and A47: a1,a4 // b1,b4 ; ::_thesis: a3,a4 // b3,b4 now__::_thesis:_(_not_M_//_N_implies_a3,a4_//_b3,b4_) assume not M // N ; ::_thesis: a3,a4 // b3,b4 then ex o being Element of X st ( o in M & o in N ) by A27, A28, AFF_1:58; hence a3,a4 // b3,b4 by A26, A27, A28, A29, A30, A31, A32, A33, A34, A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A45, A46, A47, Def2; ::_thesis: verum end; hence a3,a4 // b3,b4 by A25, A29, A30, A31, A32, A33, A34, A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A45, A46, A47, Def1; ::_thesis: verum end; hence X is satisfying_Scherungssatz by Def3; ::_thesis: verum end; ( X is satisfying_Scherungssatz implies X is satisfying_major_Scherungssatz ) proof assume X is satisfying_Scherungssatz ; ::_thesis: X is satisfying_major_Scherungssatz then for o, a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X st M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 by Def3; hence X is satisfying_major_Scherungssatz by Def2; ::_thesis: verum end; hence ( X is satisfying_Scherungssatz iff ( X is satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz ) ) by A1, A24; ::_thesis: verum end; theorem Th3: :: CONMETR1:3 for X being AffinPlane st X is satisfying_minor_indirect_Scherungssatz holds X is satisfying_minor_Scherungssatz proof let X be AffinPlane; ::_thesis: ( X is satisfying_minor_indirect_Scherungssatz implies X is satisfying_minor_Scherungssatz ) assume A1: X is satisfying_minor_indirect_Scherungssatz ; ::_thesis: X is satisfying_minor_Scherungssatz now__::_thesis:_for_a1,_a2,_a3,_a4,_b1,_b2,_b3,_b4_being_Element_of_X for_M,_N_being_Subset_of_X_st_M_//_N_&_a1_in_M_&_a3_in_M_&_b1_in_M_&_b3_in_M_&_a2_in_N_&_a4_in_N_&_b2_in_N_&_b4_in_N_&_not_a4_in_M_&_not_a2_in_M_&_not_b2_in_M_&_not_b4_in_M_&_not_a1_in_N_&_not_a3_in_N_&_not_b1_in_N_&_not_b3_in_N_&_a3,a2_//_b3,b2_&_a2,a1_//_b2,b1_&_a1,a4_//_b1,b4_holds_ a3,a4_//_b3,b4 let a1, a2, a3, a4, b1, b2, b3, b4 be Element of X; ::_thesis: for M, N being Subset of X st M // N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 let M, N be Subset of X; ::_thesis: ( M // N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 ) assume that A2: M // N and A3: a1 in M and A4: a3 in M and A5: b1 in M and A6: b3 in M and A7: a2 in N and A8: a4 in N and A9: b2 in N and A10: b4 in N and A11: not a4 in M and A12: not a2 in M and A13: not b2 in M and A14: not b4 in M and A15: not a1 in N and A16: not a3 in N and A17: not b1 in N and A18: not b3 in N and A19: a3,a2 // b3,b2 and A20: a2,a1 // b2,b1 and A21: a1,a4 // b1,b4 ; ::_thesis: a3,a4 // b3,b4 A22: N is being_line by A2, AFF_1:36; then consider d1 being Element of X such that a2 <> d1 and A23: d1 in N by AFF_1:20; A24: not d1 in M by A2, A8, A11, A23, AFF_1:45; A25: M is being_line by A2, AFF_1:36; ex d2 being Element of X st ( d2 in M & a2,a1 // d2,d1 ) proof consider e1 being Element of X such that A26: a1 <> e1 and A27: e1 in M by A25, AFF_1:20; consider e2 being Element of X such that A28: a2,a1 // d1,e2 and A29: d1 <> e2 by DIRAF:40; not a1,e1 // d1,e2 proof assume a1,e1 // d1,e2 ; ::_thesis: contradiction then a1,e1 // a2,a1 by A28, A29, AFF_1:5; then a1,e1 // a1,a2 by AFF_1:4; then LIN a1,e1,a2 by AFF_1:def_1; hence contradiction by A3, A12, A25, A26, A27, AFF_1:25; ::_thesis: verum end; then consider d2 being Element of X such that A30: LIN a1,e1,d2 and A31: LIN d1,e2,d2 by AFF_1:60; take d2 ; ::_thesis: ( d2 in M & a2,a1 // d2,d1 ) d1,e2 // d1,d2 by A31, AFF_1:def_1; then a2,a1 // d1,d2 by A28, A29, AFF_1:5; hence ( d2 in M & a2,a1 // d2,d1 ) by A3, A25, A26, A27, A30, AFF_1:4, AFF_1:25; ::_thesis: verum end; then consider d2 being Element of X such that A32: d2 in M and A33: a2,a1 // d2,d1 ; A34: not d2 in N by A2, A8, A11, A32, AFF_1:45; ex d3 being Element of X st ( d3 in N & a3,a2 // d3,d2 ) proof consider e1 being Element of X such that A35: a2 <> e1 and A36: e1 in N by A22, AFF_1:20; consider e2 being Element of X such that A37: a3,a2 // d2,e2 and A38: d2 <> e2 by DIRAF:40; not a2,e1 // d2,e2 proof assume a2,e1 // d2,e2 ; ::_thesis: contradiction then a2,e1 // a3,a2 by A37, A38, AFF_1:5; then a2,e1 // a2,a3 by AFF_1:4; then LIN a2,e1,a3 by AFF_1:def_1; hence contradiction by A7, A16, A22, A35, A36, AFF_1:25; ::_thesis: verum end; then consider d3 being Element of X such that A39: LIN a2,e1,d3 and A40: LIN d2,e2,d3 by AFF_1:60; take d3 ; ::_thesis: ( d3 in N & a3,a2 // d3,d2 ) d2,e2 // d2,d3 by A40, AFF_1:def_1; then a3,a2 // d2,d3 by A37, A38, AFF_1:5; hence ( d3 in N & a3,a2 // d3,d2 ) by A7, A22, A35, A36, A39, AFF_1:4, AFF_1:25; ::_thesis: verum end; then consider d3 being Element of X such that A41: d3 in N and A42: a3,a2 // d3,d2 ; A43: not d3 in M by A2, A8, A11, A41, AFF_1:45; ex d4 being Element of X st ( d4 in M & a1,a4 // d1,d4 ) proof consider e1 being Element of X such that A44: a1 <> e1 and A45: e1 in M by A25, AFF_1:20; consider e2 being Element of X such that A46: a1,a4 // d1,e2 and A47: d1 <> e2 by DIRAF:40; not a1,e1 // d1,e2 proof assume a1,e1 // d1,e2 ; ::_thesis: contradiction then a1,e1 // a1,a4 by A46, A47, AFF_1:5; then LIN a1,e1,a4 by AFF_1:def_1; hence contradiction by A3, A11, A25, A44, A45, AFF_1:25; ::_thesis: verum end; then consider d4 being Element of X such that A48: LIN a1,e1,d4 and A49: LIN d1,e2,d4 by AFF_1:60; take d4 ; ::_thesis: ( d4 in M & a1,a4 // d1,d4 ) d1,e2 // d1,d4 by A49, AFF_1:def_1; hence ( d4 in M & a1,a4 // d1,d4 ) by A3, A25, A44, A45, A46, A47, A48, AFF_1:5, AFF_1:25; ::_thesis: verum end; then consider d4 being Element of X such that A50: d4 in M and A51: a1,a4 // d1,d4 ; A52: not d4 in N by A2, A8, A11, A50, AFF_1:45; A53: b2,b1 // d2,d1 by A3, A12, A20, A33, AFF_1:5; A54: b1,b4 // d1,d4 by A3, A11, A21, A51, AFF_1:5; b3,b2 // d3,d2 by A4, A12, A19, A42, AFF_1:5; then A55: b3,b4 // d3,d4 by A1, A2, A5, A6, A9, A10, A13, A14, A17, A18, A23, A32, A41, A50, A24, A43, A34, A52, A53, A54, Def5; a3,a4 // d3,d4 by A1, A2, A3, A4, A7, A8, A11, A12, A15, A16, A23, A32, A33, A41, A42, A50, A51, A24, A43, A34, A52, Def5; hence a3,a4 // b3,b4 by A50, A43, A55, AFF_1:5; ::_thesis: verum end; hence X is satisfying_minor_Scherungssatz by Def1; ::_thesis: verum end; theorem Th4: :: CONMETR1:4 for X being AffinPlane st X is satisfying_major_indirect_Scherungssatz holds X is satisfying_major_Scherungssatz proof let X be AffinPlane; ::_thesis: ( X is satisfying_major_indirect_Scherungssatz implies X is satisfying_major_Scherungssatz ) assume A1: X is satisfying_major_indirect_Scherungssatz ; ::_thesis: X is satisfying_major_Scherungssatz now__::_thesis:_for_o,_a1,_a2,_a3,_a4,_b1,_b2,_b3,_b4_being_Element_of_X for_M,_N_being_Subset_of_X_st_M_is_being_line_&_N_is_being_line_&_o_in_M_&_o_in_N_&_a1_in_M_&_a3_in_M_&_b1_in_M_&_b3_in_M_&_a2_in_N_&_a4_in_N_&_b2_in_N_&_b4_in_N_&_not_a4_in_M_&_not_a2_in_M_&_not_b2_in_M_&_not_b4_in_M_&_not_a1_in_N_&_not_a3_in_N_&_not_b1_in_N_&_not_b3_in_N_&_a3,a2_//_b3,b2_&_a2,a1_//_b2,b1_&_a1,a4_//_b1,b4_holds_ a3,a4_//_b3,b4 let o, a1, a2, a3, a4, b1, b2, b3, b4 be Element of X; ::_thesis: for M, N being Subset of X st M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 let M, N be Subset of X; ::_thesis: ( M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 ) assume that A2: M is being_line and A3: N is being_line and A4: o in M and A5: o in N and A6: a1 in M and A7: a3 in M and A8: b1 in M and A9: b3 in M and A10: a2 in N and A11: a4 in N and A12: b2 in N and A13: b4 in N and A14: not a4 in M and A15: not a2 in M and A16: not b2 in M and A17: not b4 in M and A18: not a1 in N and A19: not a3 in N and A20: not b1 in N and A21: not b3 in N and A22: a3,a2 // b3,b2 and A23: a2,a1 // b2,b1 and A24: a1,a4 // b1,b4 ; ::_thesis: a3,a4 // b3,b4 A25: now__::_thesis:_(_a1_<>_a3_&_a2_<>_a4_implies_a3,a4_//_b3,b4_) assume that A26: a1 <> a3 and A27: a2 <> a4 ; ::_thesis: a3,a4 // b3,b4 consider d1 being Element of X such that A28: o <> d1 and A29: d1 in N by A4, A11, A14; A30: ex d4 being Element of X st ( d4 in M & a1,a4 // d1,d4 ) proof consider e1 being Element of X such that A31: o <> e1 and A32: e1 in M by A5, A6, A18; consider e2 being Element of X such that A33: a1,a4 // d1,e2 and A34: d1 <> e2 by DIRAF:40; not o,e1 // d1,e2 proof assume o,e1 // d1,e2 ; ::_thesis: contradiction then A35: o,e1 // a1,a4 by A33, A34, AFF_1:5; o,e1 // a1,a3 by A2, A4, A6, A7, A32, AFF_1:39, AFF_1:41; then a1,a3 // a1,a4 by A31, A35, AFF_1:5; then LIN a1,a3,a4 by AFF_1:def_1; hence contradiction by A2, A6, A7, A14, A26, AFF_1:25; ::_thesis: verum end; then consider d4 being Element of X such that A36: LIN o,e1,d4 and A37: LIN d1,e2,d4 by AFF_1:60; take d4 ; ::_thesis: ( d4 in M & a1,a4 // d1,d4 ) d1,e2 // d1,d4 by A37, AFF_1:def_1; hence ( d4 in M & a1,a4 // d1,d4 ) by A2, A4, A31, A32, A33, A34, A36, AFF_1:5, AFF_1:25; ::_thesis: verum end; A38: ex d2 being Element of X st ( d2 in M & a2,a1 // d2,d1 ) proof consider e1 being Element of X such that A39: o <> e1 and A40: e1 in M by A5, A6, A18; consider e2 being Element of X such that A41: a2,a1 // d1,e2 and A42: d1 <> e2 by DIRAF:40; not o,e1 // d1,e2 proof assume o,e1 // d1,e2 ; ::_thesis: contradiction then A43: o,e1 // a2,a1 by A41, A42, AFF_1:5; o,e1 // a1,a3 by A2, A4, A6, A7, A40, AFF_1:39, AFF_1:41; then a1,a3 // a2,a1 by A39, A43, AFF_1:5; then a1,a3 // a1,a2 by AFF_1:4; then LIN a1,a3,a2 by AFF_1:def_1; hence contradiction by A2, A6, A7, A15, A26, AFF_1:25; ::_thesis: verum end; then consider d2 being Element of X such that A44: LIN o,e1,d2 and A45: LIN d1,e2,d2 by AFF_1:60; take d2 ; ::_thesis: ( d2 in M & a2,a1 // d2,d1 ) d1,e2 // d1,d2 by A45, AFF_1:def_1; then a2,a1 // d1,d2 by A41, A42, AFF_1:5; hence ( d2 in M & a2,a1 // d2,d1 ) by A2, A4, A39, A40, A44, AFF_1:4, AFF_1:25; ::_thesis: verum end; consider d4 being Element of X such that A46: d4 in M and A47: a1,a4 // d1,d4 by A30; consider d2 being Element of X such that A48: d2 in M and A49: a2,a1 // d2,d1 by A38; A50: b2,b1 // d2,d1 by A6, A15, A23, A49, AFF_1:5; ex d3 being Element of X st ( d3 in N & a3,a2 // d3,d2 ) proof consider e1 being Element of X such that A51: o <> e1 and A52: e1 in N by A4, A11, A14; consider e2 being Element of X such that A53: a3,a2 // d2,e2 and A54: d2 <> e2 by DIRAF:40; not o,e1 // d2,e2 proof assume o,e1 // d2,e2 ; ::_thesis: contradiction then A55: o,e1 // a3,a2 by A53, A54, AFF_1:5; o,e1 // a2,a4 by A3, A5, A10, A11, A52, AFF_1:39, AFF_1:41; then a2,a4 // a3,a2 by A51, A55, AFF_1:5; then a2,a4 // a2,a3 by AFF_1:4; then LIN a2,a4,a3 by AFF_1:def_1; hence contradiction by A3, A10, A11, A19, A27, AFF_1:25; ::_thesis: verum end; then consider d3 being Element of X such that A56: LIN o,e1,d3 and A57: LIN d2,e2,d3 by AFF_1:60; take d3 ; ::_thesis: ( d3 in N & a3,a2 // d3,d2 ) d2,e2 // d2,d3 by A57, AFF_1:def_1; then a3,a2 // d2,d3 by A53, A54, AFF_1:5; hence ( d3 in N & a3,a2 // d3,d2 ) by A3, A5, A51, A52, A56, AFF_1:4, AFF_1:25; ::_thesis: verum end; then consider d3 being Element of X such that A58: d3 in N and A59: a3,a2 // d3,d2 ; A60: ( d2 <> o & d3 <> o & d4 <> o ) proof A61: now__::_thesis:_not_d4_=_o assume A62: d4 = o ; ::_thesis: contradiction d1,o // a2,a4 by A3, A5, A10, A11, A29, AFF_1:39, AFF_1:41; then a1,a4 // a2,a4 by A28, A47, A62, AFF_1:5; then a4,a2 // a4,a1 by AFF_1:4; then LIN a4,a2,a1 by AFF_1:def_1; hence contradiction by A3, A10, A11, A18, A27, AFF_1:25; ::_thesis: verum end; A63: now__::_thesis:_not_d2_=_o assume A64: d2 = o ; ::_thesis: contradiction o,d1 // a2,a4 by A3, A5, A10, A11, A29, AFF_1:39, AFF_1:41; then a2,a4 // a2,a1 by A28, A49, A64, AFF_1:5; then LIN a2,a4,a1 by AFF_1:def_1; hence contradiction by A3, A10, A11, A18, A27, AFF_1:25; ::_thesis: verum end; A65: now__::_thesis:_not_d3_=_o assume A66: d3 = o ; ::_thesis: contradiction o,d2 // a3,a1 by A2, A4, A6, A7, A48, AFF_1:39, AFF_1:41; then a3,a1 // a3,a2 by A59, A63, A66, AFF_1:5; then LIN a3,a1,a2 by AFF_1:def_1; hence contradiction by A2, A6, A7, A15, A26, AFF_1:25; ::_thesis: verum end; assume ( not d2 <> o or not d3 <> o or not d4 <> o ) ; ::_thesis: contradiction hence contradiction by A63, A65, A61; ::_thesis: verum end; A67: ( not d1 in M & not d3 in M & not d2 in N & not d4 in N ) proof assume ( d1 in M or d3 in M or d2 in N or d4 in N ) ; ::_thesis: contradiction then A68: ( o,d1 // M or o,d3 // M or o,d2 // N or o,d4 // N ) by A2, A3, A4, A5, AFF_1:52; A69: o,d3 // N by A3, A5, A58, AFF_1:52; A70: o,d4 // M by A2, A4, A46, AFF_1:52; A71: o,d2 // M by A2, A4, A48, AFF_1:52; o,d1 // N by A3, A5, A29, AFF_1:52; hence contradiction by A4, A5, A11, A14, A28, A60, A68, A69, A71, A70, AFF_1:45, AFF_1:53; ::_thesis: verum end; A72: b1,b4 // d1,d4 by A6, A14, A24, A47, AFF_1:5; A73: ( d1 <> d2 & d2 <> d3 & d3 <> d4 & d4 <> d1 ) proof assume ( not d1 <> d2 or not d2 <> d3 or not d3 <> d4 or not d4 <> d1 ) ; ::_thesis: contradiction then A74: ( o,d1 // M or o,d3 // M ) by A2, A4, A48, A46, AFF_1:52; A75: o,d3 // N by A3, A5, A58, AFF_1:52; o,d1 // N by A3, A5, A29, AFF_1:52; hence contradiction by A4, A5, A11, A14, A28, A60, A74, A75, AFF_1:45, AFF_1:53; ::_thesis: verum end; b3,b2 // d3,d2 by A7, A15, A22, A59, AFF_1:5; then A76: b3,b4 // d3,d4 by A1, A2, A3, A4, A5, A8, A9, A12, A13, A16, A17, A20, A21, A29, A48, A58, A46, A67, A50, A72, Def6; a3,a4 // d3,d4 by A1, A2, A3, A4, A5, A6, A7, A10, A11, A14, A15, A18, A19, A29, A48, A49, A58, A59, A46, A47, A67, Def6; hence a3,a4 // b3,b4 by A73, A76, AFF_1:5; ::_thesis: verum end; now__::_thesis:_(_(_a1_=_a3_or_a2_=_a4_)_implies_a3,a4_//_b3,b4_) A77: now__::_thesis:_(_a2_=_a4_implies_a3,a4_//_b3,b4_) o,b2 // o,b4 by A3, A5, A12, A13, AFF_1:39, AFF_1:41; then A78: LIN o,b2,b4 by AFF_1:def_1; assume A79: a2 = a4 ; ::_thesis: a3,a4 // b3,b4 then a1,a4 // b1,b2 by A23, AFF_1:4; then b1,b2 // b1,b4 by A6, A14, A24, AFF_1:5; hence a3,a4 // b3,b4 by A2, A4, A5, A8, A16, A20, A22, A79, A78, AFF_1:14, AFF_1:25; ::_thesis: verum end; A80: now__::_thesis:_(_a1_=_a3_implies_a3,a4_//_b3,b4_) o,b1 // o,b3 by A2, A4, A8, A9, AFF_1:39, AFF_1:41; then A81: LIN o,b1,b3 by AFF_1:def_1; assume A82: a1 = a3 ; ::_thesis: a3,a4 // b3,b4 then a2,a1 // b2,b3 by A22, AFF_1:4; then b2,b1 // b2,b3 by A6, A15, A23, AFF_1:5; hence a3,a4 // b3,b4 by A3, A4, A5, A12, A16, A20, A24, A82, A81, AFF_1:14, AFF_1:25; ::_thesis: verum end; assume ( a1 = a3 or a2 = a4 ) ; ::_thesis: a3,a4 // b3,b4 hence a3,a4 // b3,b4 by A80, A77; ::_thesis: verum end; hence a3,a4 // b3,b4 by A25; ::_thesis: verum end; hence X is satisfying_major_Scherungssatz by Def2; ::_thesis: verum end; theorem :: CONMETR1:5 for X being AffinPlane st X is satisfying_indirect_Scherungssatz holds X is satisfying_Scherungssatz proof let X be AffinPlane; ::_thesis: ( X is satisfying_indirect_Scherungssatz implies X is satisfying_Scherungssatz ) assume A1: X is satisfying_indirect_Scherungssatz ; ::_thesis: X is satisfying_Scherungssatz then X is satisfying_major_indirect_Scherungssatz by Th1; then A2: X is satisfying_major_Scherungssatz by Th4; X is satisfying_minor_indirect_Scherungssatz by A1, Th1; then X is satisfying_minor_Scherungssatz by Th3; hence X is satisfying_Scherungssatz by A2, Th2; ::_thesis: verum end; theorem Th6: :: CONMETR1:6 for X being AffinPlane st X is translational holds X is satisfying_minor_Scherungssatz proof let X be AffinPlane; ::_thesis: ( X is translational implies X is satisfying_minor_Scherungssatz ) assume A1: X is translational ; ::_thesis: X is satisfying_minor_Scherungssatz now__::_thesis:_for_a1,_a2,_a3,_a4,_b1,_b2,_b3,_b4_being_Element_of_X for_M,_N_being_Subset_of_X_st_M_//_N_&_a1_in_M_&_a3_in_M_&_b1_in_M_&_b3_in_M_&_a2_in_N_&_a4_in_N_&_b2_in_N_&_b4_in_N_&_not_a4_in_M_&_not_a2_in_M_&_not_b2_in_M_&_not_b4_in_M_&_not_a1_in_N_&_not_a3_in_N_&_not_b1_in_N_&_not_b3_in_N_&_a3,a2_//_b3,b2_&_a2,a1_//_b2,b1_&_a1,a4_//_b1,b4_holds_ a3,a4_//_b3,b4 let a1, a2, a3, a4, b1, b2, b3, b4 be Element of X; ::_thesis: for M, N being Subset of X st M // N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 let M, N be Subset of X; ::_thesis: ( M // N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 ) assume that A2: M // N and A3: a1 in M and A4: a3 in M and A5: b1 in M and A6: b3 in M and A7: a2 in N and A8: a4 in N and A9: b2 in N and A10: b4 in N and A11: not a4 in M and A12: not a2 in M and A13: not b2 in M and not b4 in M and A14: not a1 in N and A15: not a3 in N and A16: not b1 in N and not b3 in N and A17: a3,a2 // b3,b2 and A18: a2,a1 // b2,b1 and A19: a1,a4 // b1,b4 ; ::_thesis: a3,a4 // b3,b4 A20: M is being_line by A2, AFF_1:36; A21: N is being_line by A2, AFF_1:36; A22: now__::_thesis:_(_a1_<>_a3_&_a2_<>_a4_implies_a3,a4_//_b3,b4_) assume that A23: a1 <> a3 and A24: a2 <> a4 ; ::_thesis: a3,a4 // b3,b4 A25: now__::_thesis:_(_ex_x,_y,_z_being_Element_of_X_st_ (_LIN_x,y,z_&_x_<>_y_&_x_<>_z_&_y_<>_z_)_implies_a3,a4_//_b3,b4_) assume ex x, y, z being Element of X st ( LIN x,y,z & x <> y & x <> z & y <> z ) ; ::_thesis: a3,a4 // b3,b4 then consider d being Element of X such that A26: LIN a1,a2,d and A27: a1 <> d and A28: a2 <> d by TRANSLAC:1; A29: ex Y being Subset of X st ( Y is being_line & d in Y & Y // M ) proof consider Y being Subset of X such that A30: d in Y and A31: M // Y by A20, AFF_1:49; take Y ; ::_thesis: ( Y is being_line & d in Y & Y // M ) thus ( Y is being_line & d in Y & Y // M ) by A30, A31, AFF_1:36; ::_thesis: verum end; LIN a2,a1,d by A26, AFF_1:6; then a2,a1 // a2,d by AFF_1:def_1; then A32: b2,b1 // a2,d by A3, A12, A18, AFF_1:5; A33: a2,a3 // b2,b3 by A17, AFF_1:4; consider Y being Subset of X such that A34: Y is being_line and A35: d in Y and A36: Y // M by A29; A37: Y // N by A2, A36, AFF_1:44; A38: ( N <> M & N <> Y & Y <> M ) proof A39: now__::_thesis:_not_N_=_Y LIN a2,d,a1 by A26, AFF_1:6; then A40: a2,d // a2,a1 by AFF_1:def_1; assume N = Y ; ::_thesis: contradiction then a2,d // a2,a4 by A7, A8, A34, A35, AFF_1:39, AFF_1:41; then a2,a4 // a2,a1 by A28, A40, AFF_1:5; then LIN a2,a4,a1 by AFF_1:def_1; hence contradiction by A7, A8, A14, A21, A24, AFF_1:25; ::_thesis: verum end; A41: now__::_thesis:_not_Y_=_M assume Y = M ; ::_thesis: contradiction then A42: a1,d // a1,a3 by A3, A4, A35, A36, AFF_1:39; a1,a2 // a1,d by A26, AFF_1:def_1; then a1,a3 // a1,a2 by A27, A42, AFF_1:5; then LIN a1,a3,a2 by AFF_1:def_1; hence contradiction by A3, A4, A12, A20, A23, AFF_1:25; ::_thesis: verum end; assume ( not N <> M or not N <> Y or not Y <> M ) ; ::_thesis: contradiction hence contradiction by A8, A11, A39, A41; ::_thesis: verum end; A43: Y // Y by A34, AFF_1:41; ex d1 being Element of X st ( d1 in Y & b1,b2 // b1,d1 ) proof consider e1 being Element of X such that A44: d <> e1 and A45: e1 in Y by A34, AFF_1:20; consider e2 being Element of X such that A46: b1,b2 // b1,e2 and A47: b1 <> e2 by DIRAF:40; not d,e1 // b1,e2 proof assume d,e1 // b1,e2 ; ::_thesis: contradiction then d,e1 // b1,b2 by A46, A47, AFF_1:5; then A48: b1,b2 // Y by A35, A43, A44, A45, AFF_1:32, AFF_1:40; a1,a3 // Y by A3, A4, A36, AFF_1:40; then a1,a3 // b1,b2 by A34, A48, AFF_1:31; then a1,a3 // b2,b1 by AFF_1:4; then a1,a3 // a2,a1 by A5, A13, A18, AFF_1:5; then a1,a3 // a1,a2 by AFF_1:4; then LIN a1,a3,a2 by AFF_1:def_1; hence contradiction by A3, A4, A12, A20, A23, AFF_1:25; ::_thesis: verum end; then consider d1 being Element of X such that A49: LIN d,e1,d1 and A50: LIN b1,e2,d1 by AFF_1:60; take d1 ; ::_thesis: ( d1 in Y & b1,b2 // b1,d1 ) b1,e2 // b1,d1 by A50, AFF_1:def_1; hence ( d1 in Y & b1,b2 // b1,d1 ) by A34, A35, A44, A45, A46, A47, A49, AFF_1:5, AFF_1:25; ::_thesis: verum end; then consider d1 being Element of X such that A51: d1 in Y and A52: b1,b2 // b1,d1 ; a1,a2 // a1,d by A26, AFF_1:def_1; then a2,a1 // a1,d by AFF_1:4; then b2,b1 // a1,d by A3, A12, A18, AFF_1:5; then b1,b2 // a1,d by AFF_1:4; then a1,d // b1,d1 by A5, A13, A52, AFF_1:5; then A53: d,a4 // d1,b4 by A1, A2, A3, A5, A8, A10, A19, A20, A21, A34, A35, A36, A51, A38, AFF_2:def_11; LIN b1,b2,d1 by A52, AFF_1:def_1; then LIN b2,b1,d1 by AFF_1:6; then b2,b1 // b2,d1 by AFF_1:def_1; then A54: a2,d // b2,d1 by A5, A13, A32, AFF_1:5; N // Y by A2, A36, AFF_1:44; then d,a3 // d1,b3 by A1, A2, A4, A6, A7, A9, A20, A21, A34, A35, A51, A38, A54, A33, AFF_2:def_11; hence a3,a4 // b3,b4 by A1, A4, A6, A8, A10, A20, A21, A34, A35, A36, A51, A38, A53, A37, AFF_2:def_11; ::_thesis: verum end; now__::_thesis:_(_(_for_x,_y,_z_being_Element_of_X_holds_ (_not_LIN_x,y,z_or_not_x_<>_y_or_not_x_<>_z_or_not_y_<>_z_)_)_implies_a3,a4_//_b3,b4_) assume A55: for x, y, z being Element of X holds ( not LIN x,y,z or not x <> y or not x <> z or not y <> z ) ; ::_thesis: a3,a4 // b3,b4 A56: now__::_thesis:_(_a1_=_b1_implies_a3,a4_//_b3,b4_) assume A57: a1 = b1 ; ::_thesis: a3,a4 // b3,b4 then A58: LIN a1,a4,b4 by A19, AFF_1:def_1; a1,a2 // a1,b2 by A18, A57, AFF_1:4; then A59: LIN a1,a2,b2 by AFF_1:def_1; a2,b2 // M by A2, A7, A9, AFF_1:40; then a2 = b2 by A3, A12, A59, AFF_1:46; then a2,a3 // a2,b3 by A17, AFF_1:4; then A60: LIN a2,a3,b3 by AFF_1:def_1; a3,b3 // N by A2, A4, A6, AFF_1:40; then A61: a3 = b3 by A7, A15, A60, AFF_1:46; a4,b4 // M by A2, A8, A10, AFF_1:40; then a4 = b4 by A3, A11, A58, AFF_1:46; hence a3,a4 // b3,b4 by A61, AFF_1:2; ::_thesis: verum end; A62: now__::_thesis:_(_a3_=_b1_implies_a3,a4_//_b3,b4_) assume A63: a3 = b1 ; ::_thesis: a3,a4 // b3,b4 A64: now__::_thesis:_(_a4_=_b2_implies_a3,a4_//_b3,b4_) A65: a4 <> b4 proof assume a4 = b4 ; ::_thesis: contradiction then a4,a1 // a4,b1 by A19, AFF_1:4; then A66: LIN a4,a1,b1 by AFF_1:def_1; a1,b1 // N by A2, A3, A5, AFF_1:40; hence contradiction by A8, A14, A23, A63, A66, AFF_1:46; ::_thesis: verum end; a2,a4 // a2,b4 by A7, A8, A10, A21, AFF_1:39, AFF_1:41; then LIN a2,a4,b4 by AFF_1:def_1; then A67: a2 = b4 by A24, A55, A65; assume A68: a4 = b2 ; ::_thesis: a3,a4 // b3,b4 A69: a3 <> b3 proof assume a3 = b3 ; ::_thesis: contradiction then A70: LIN a3,a2,b2 by A17, AFF_1:def_1; a2,b2 // M by A2, A7, A9, AFF_1:40; hence contradiction by A4, A12, A24, A68, A70, AFF_1:46; ::_thesis: verum end; a1,a3 // a1,b3 by A3, A4, A6, A20, AFF_1:39, AFF_1:41; then LIN a1,a3,b3 by AFF_1:def_1; then A71: a1 = b3 by A23, A55, A69; a3,a4 // b2,b1 by A63, A68, AFF_1:2; then a3,a4 // a2,a1 by A5, A13, A18, AFF_1:5; hence a3,a4 // b3,b4 by A71, A67, AFF_1:4; ::_thesis: verum end; A72: now__::_thesis:_(_a2_=_b2_implies_a3,a4_//_b3,b4_) assume a2 = b2 ; ::_thesis: a3,a4 // b3,b4 then A73: LIN a2,a1,b1 by A18, AFF_1:def_1; a1,b1 // N by A2, A3, A5, AFF_1:40; hence a3,a4 // b3,b4 by A7, A14, A56, A73, AFF_1:46; ::_thesis: verum end; a2,a4 // a2,b2 by A7, A8, A9, A21, AFF_1:39, AFF_1:41; then LIN a2,a4,b2 by AFF_1:def_1; hence a3,a4 // b3,b4 by A24, A55, A64, A72; ::_thesis: verum end; a1,a3 // a1,b1 by A3, A4, A5, A20, AFF_1:39, AFF_1:41; then LIN a1,a3,b1 by AFF_1:def_1; hence a3,a4 // b3,b4 by A23, A55, A56, A62; ::_thesis: verum end; hence a3,a4 // b3,b4 by A25; ::_thesis: verum end; now__::_thesis:_(_(_a1_=_a3_or_a2_=_a4_)_implies_a3,a4_//_b3,b4_) A74: now__::_thesis:_(_a1_=_a3_implies_a3,a4_//_b3,b4_) assume A75: a1 = a3 ; ::_thesis: a3,a4 // b3,b4 b1 = b3 proof LIN a2,a1,a3 by A75, AFF_1:7; then a2,a1 // a2,a3 by AFF_1:def_1; then b2,b1 // a2,a3 by A3, A12, A18, AFF_1:5; then b2,b1 // a3,a2 by AFF_1:4; then b2,b1 // b3,b2 by A4, A12, A17, AFF_1:5; then b2,b1 // b2,b3 by AFF_1:4; then A76: LIN b2,b1,b3 by AFF_1:def_1; assume A77: b1 <> b3 ; ::_thesis: contradiction b1,b3 // N by A2, A5, A6, AFF_1:40; hence contradiction by A9, A16, A77, A76, AFF_1:46; ::_thesis: verum end; hence a3,a4 // b3,b4 by A19, A75; ::_thesis: verum end; A78: now__::_thesis:_(_a2_=_a4_implies_a3,a4_//_b3,b4_) assume A79: a2 = a4 ; ::_thesis: a3,a4 // b3,b4 then LIN a1,a4,a2 by AFF_1:7; then a1,a4 // a1,a2 by AFF_1:def_1; then b1,b4 // a1,a2 by A3, A11, A19, AFF_1:5; then b1,b4 // a2,a1 by AFF_1:4; then b1,b4 // b2,b1 by A3, A12, A18, AFF_1:5; then b1,b2 // b1,b4 by AFF_1:4; then A80: LIN b1,b2,b4 by AFF_1:def_1; b2,b4 // M by A2, A9, A10, AFF_1:40; hence a3,a4 // b3,b4 by A5, A13, A17, A79, A80, AFF_1:46; ::_thesis: verum end; assume ( a1 = a3 or a2 = a4 ) ; ::_thesis: a3,a4 // b3,b4 hence a3,a4 // b3,b4 by A74, A78; ::_thesis: verum end; hence a3,a4 // b3,b4 by A22; ::_thesis: verum end; hence X is satisfying_minor_Scherungssatz by Def1; ::_thesis: verum end; theorem Th7: :: CONMETR1:7 for X being AffinPlane st X is Desarguesian holds X is satisfying_major_Scherungssatz proof let X be AffinPlane; ::_thesis: ( X is Desarguesian implies X is satisfying_major_Scherungssatz ) assume A1: X is Desarguesian ; ::_thesis: X is satisfying_major_Scherungssatz now__::_thesis:_for_o,_a1,_a2,_a3,_a4,_b1,_b2,_b3,_b4_being_Element_of_X for_M,_N_being_Subset_of_X_st_M_is_being_line_&_N_is_being_line_&_o_in_M_&_o_in_N_&_a1_in_M_&_a3_in_M_&_b1_in_M_&_b3_in_M_&_a2_in_N_&_a4_in_N_&_b2_in_N_&_b4_in_N_&_not_a4_in_M_&_not_a2_in_M_&_not_b2_in_M_&_not_b4_in_M_&_not_a1_in_N_&_not_a3_in_N_&_not_b1_in_N_&_not_b3_in_N_&_a3,a2_//_b3,b2_&_a2,a1_//_b2,b1_&_a1,a4_//_b1,b4_holds_ a3,a4_//_b3,b4 let o, a1, a2, a3, a4, b1, b2, b3, b4 be Element of X; ::_thesis: for M, N being Subset of X st M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 let M, N be Subset of X; ::_thesis: ( M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 ) assume that A2: M is being_line and A3: N is being_line and A4: o in M and A5: o in N and A6: a1 in M and A7: a3 in M and A8: b1 in M and A9: b3 in M and A10: a2 in N and A11: a4 in N and A12: b2 in N and A13: b4 in N and A14: not a4 in M and A15: not a2 in M and A16: not b2 in M and not b4 in M and A17: not a1 in N and A18: not a3 in N and A19: not b1 in N and not b3 in N and A20: a3,a2 // b3,b2 and A21: a2,a1 // b2,b1 and A22: a1,a4 // b1,b4 ; ::_thesis: a3,a4 // b3,b4 A23: now__::_thesis:_(_a1_<>_a3_&_a2_<>_a4_implies_a3,a4_//_b3,b4_) A24: now__::_thesis:_(_ex_x,_y,_z_being_Element_of_X_st_ (_LIN_x,y,z_&_x_<>_y_&_x_<>_z_&_y_<>_z_)_implies_a3,a4_//_b3,b4_) assume ex x, y, z being Element of X st ( LIN x,y,z & x <> y & x <> z & y <> z ) ; ::_thesis: a3,a4 // b3,b4 then consider d being Element of X such that A25: LIN a1,a2,d and A26: a1 <> d and A27: a2 <> d by TRANSLAC:1; LIN o,d,d by AFF_1:7; then consider Y being Subset of X such that A28: Y is being_line and A29: o in Y and A30: d in Y and d in Y by AFF_1:21; a1,a2 // a1,d by A25, AFF_1:def_1; then a2,a1 // a1,d by AFF_1:4; then A31: b2,b1 // a1,d by A6, A15, A21, AFF_1:5; A32: ( N <> M & N <> Y & M <> Y ) proof A33: now__::_thesis:_(_not_N_=_Y_&_not_M_=_Y_) A34: LIN a1,d,a2 by A25, AFF_1:6; assume A35: ( N = Y or M = Y ) ; ::_thesis: contradiction LIN a2,d,a1 by A25, AFF_1:6; hence contradiction by A2, A3, A6, A10, A15, A17, A26, A27, A30, A35, A34, AFF_1:25; ::_thesis: verum end; assume ( not N <> M or not N <> Y or not M <> Y ) ; ::_thesis: contradiction hence contradiction by A11, A14, A33; ::_thesis: verum end; A36: ex d1 being Element of X st ( LIN b1,b2,d1 & d1 in Y ) proof not b1,b2 // o,d proof A37: o <> d proof assume o = d ; ::_thesis: contradiction then LIN o,a1,a2 by A25, AFF_1:6; hence contradiction by A2, A4, A5, A6, A15, A17, AFF_1:25; ::_thesis: verum end; assume b1,b2 // o,d ; ::_thesis: contradiction then b2,b1 // o,d by AFF_1:4; then A38: a2,a1 // o,d by A8, A16, A21, AFF_1:5; a1,a2 // a1,d by A25, AFF_1:def_1; then a2,a1 // a1,d by AFF_1:4; then a1,d // o,d by A6, A15, A38, AFF_1:5; then d,o // d,a1 by AFF_1:4; then LIN d,o,a1 by AFF_1:def_1; then LIN o,d,a1 by AFF_1:6; then o,d // o,a1 by AFF_1:def_1; then A39: Y // M by A2, A4, A5, A6, A17, A28, A29, A30, A37, AFF_1:38; LIN a2,a1,d by A25, AFF_1:6; then a2,a1 // a2,d by AFF_1:def_1; then a2,d // o,d by A6, A15, A38, AFF_1:5; then d,a2 // d,o by AFF_1:4; then LIN d,a2,o by AFF_1:def_1; then LIN o,d,a2 by AFF_1:6; then o,d // o,a2 by AFF_1:def_1; then Y // N by A3, A4, A5, A10, A15, A28, A29, A30, A37, AFF_1:38; then M // N by A39, AFF_1:44; hence contradiction by A4, A5, A11, A14, AFF_1:45; ::_thesis: verum end; then consider d1 being Element of X such that A40: LIN b1,b2,d1 and A41: LIN o,d,d1 by AFF_1:60; take d1 ; ::_thesis: ( LIN b1,b2,d1 & d1 in Y ) o <> d proof assume o = d ; ::_thesis: contradiction then LIN o,a1,a2 by A25, AFF_1:6; hence contradiction by A2, A4, A5, A6, A15, A17, AFF_1:25; ::_thesis: verum end; hence ( LIN b1,b2,d1 & d1 in Y ) by A28, A29, A30, A40, A41, AFF_1:25; ::_thesis: verum end; LIN a2,a1,d by A25, AFF_1:6; then a2,a1 // a2,d by AFF_1:def_1; then A42: b2,b1 // a2,d by A6, A15, A21, AFF_1:5; A43: o <> d proof assume o = d ; ::_thesis: contradiction then LIN o,a1,a2 by A25, AFF_1:6; hence contradiction by A2, A4, A5, A6, A15, A17, AFF_1:25; ::_thesis: verum end; consider d1 being Element of X such that A44: LIN b1,b2,d1 and A45: d1 in Y by A36; b1,b2 // b1,d1 by A44, AFF_1:def_1; then b2,b1 // b1,d1 by AFF_1:4; then a1,d // b1,d1 by A8, A16, A31, AFF_1:5; then A46: d,a4 // d1,b4 by A1, A2, A3, A4, A5, A6, A8, A11, A13, A14, A17, A22, A28, A29, A30, A45, A43, A32, AFF_2:def_4; LIN b2,b1,d1 by A44, AFF_1:6; then b2,b1 // b2,d1 by AFF_1:def_1; then A47: a2,d // b2,d1 by A8, A16, A42, AFF_1:5; a2,a3 // b2,b3 by A20, AFF_1:4; then d,a3 // d1,b3 by A1, A2, A3, A4, A5, A7, A9, A10, A12, A15, A18, A28, A29, A30, A45, A43, A32, A47, AFF_2:def_4; hence a3,a4 // b3,b4 by A1, A2, A3, A4, A5, A7, A9, A11, A13, A14, A18, A28, A29, A30, A45, A43, A32, A46, AFF_2:def_4; ::_thesis: verum end; assume that A48: a1 <> a3 and A49: a2 <> a4 ; ::_thesis: a3,a4 // b3,b4 now__::_thesis:_(_(_for_x,_y,_z_being_Element_of_X_holds_ (_not_LIN_x,y,z_or_not_x_<>_y_or_not_x_<>_z_or_not_y_<>_z_)_)_implies_a3,a4_//_b3,b4_) assume A50: for x, y, z being Element of X holds ( not LIN x,y,z or not x <> y or not x <> z or not y <> z ) ; ::_thesis: a3,a4 // b3,b4 A51: now__::_thesis:_(_a1_=_b1_implies_a3,a4_//_b3,b4_) assume A52: a1 = b1 ; ::_thesis: a3,a4 // b3,b4 A53: a2 <> b4 proof assume a2 = b4 ; ::_thesis: contradiction then LIN a1,a4,a2 by A22, A52, AFF_1:def_1; then LIN a2,a4,a1 by AFF_1:6; hence contradiction by A3, A10, A11, A17, A49, AFF_1:25; ::_thesis: verum end; A54: a1 <> b3 proof assume a1 = b3 ; ::_thesis: contradiction then b2,b1 // a2,a3 by A20, A52, AFF_1:4; then A55: a2,a1 // a2,a3 by A8, A16, A21, AFF_1:5; LIN o,a1,a3 by A2, A4, A6, A7, AFF_1:21; hence contradiction by A3, A4, A5, A10, A15, A17, A48, A55, AFF_1:14, AFF_1:25; ::_thesis: verum end; LIN a2,a4,b4 by A3, A10, A11, A13, AFF_1:21; then A56: ( a2 = b4 or a4 = b4 ) by A49, A50; LIN a1,a3,b3 by A2, A6, A7, A9, AFF_1:21; then a3 = b3 by A48, A50, A54; hence a3,a4 // b3,b4 by A56, A53, AFF_1:2; ::_thesis: verum end; A57: now__::_thesis:_(_a3_=_b1_implies_a3,a4_//_b3,b4_) assume A58: a3 = b1 ; ::_thesis: a3,a4 // b3,b4 A59: a2 <> b2 proof assume a2 = b2 ; ::_thesis: contradiction then LIN a2,a1,a3 by A21, A58, AFF_1:def_1; then LIN a1,a3,a2 by AFF_1:6; hence contradiction by A2, A6, A7, A15, A48, AFF_1:25; ::_thesis: verum end; A60: a3 <> b3 proof assume a3 = b3 ; ::_thesis: contradiction then a3,a2 // b2,b1 by A20, A58, AFF_1:4; then a3,a2 // a2,a1 by A8, A16, A21, AFF_1:5; then a2,a3 // a2,a1 by AFF_1:4; then LIN a2,a3,a1 by AFF_1:def_1; then LIN a1,a3,a2 by AFF_1:6; hence contradiction by A2, A6, A7, A15, A48, AFF_1:25; ::_thesis: verum end; A61: a4 <> b4 proof assume a4 = b4 ; ::_thesis: contradiction then a4,a1 // a4,a3 by A22, A58, AFF_1:4; then LIN a4,a1,a3 by AFF_1:def_1; then LIN a1,a3,a4 by AFF_1:6; hence contradiction by A2, A6, A7, A14, A48, AFF_1:25; ::_thesis: verum end; LIN a2,a4,b4 by A3, A10, A11, A13, AFF_1:21; then A62: a2 = b4 by A49, A50, A61; LIN a2,a4,b2 by A3, A10, A11, A12, AFF_1:21; then a4 = b2 by A49, A50, A59; then A63: a3,a4 // b2,b1 by A58, AFF_1:2; LIN a1,a3,b3 by A2, A6, A7, A9, AFF_1:21; then a1 = b3 by A48, A50, A60; then a3,a4 // b4,b3 by A8, A16, A21, A62, A63, AFF_1:5; hence a3,a4 // b3,b4 by AFF_1:4; ::_thesis: verum end; LIN a1,a3,b1 by A2, A6, A7, A8, AFF_1:21; hence a3,a4 // b3,b4 by A48, A50, A51, A57; ::_thesis: verum end; hence a3,a4 // b3,b4 by A24; ::_thesis: verum end; now__::_thesis:_(_(_a1_=_a3_or_a2_=_a4_)_implies_a3,a4_//_b3,b4_) A64: now__::_thesis:_(_a2_=_a4_implies_a3,a4_//_b3,b4_) o,b2 // o,b4 by A3, A5, A12, A13, AFF_1:39, AFF_1:41; then A65: LIN o,b2,b4 by AFF_1:def_1; assume A66: a2 = a4 ; ::_thesis: a3,a4 // b3,b4 a1,a2 // b1,b2 by A21, AFF_1:4; then b1,b2 // b1,b4 by A6, A14, A22, A66, AFF_1:5; hence a3,a4 // b3,b4 by A2, A4, A5, A8, A16, A19, A20, A66, A65, AFF_1:14, AFF_1:25; ::_thesis: verum end; A67: now__::_thesis:_(_a1_=_a3_implies_a3,a4_//_b3,b4_) o,b1 // o,b3 by A2, A4, A8, A9, AFF_1:39, AFF_1:41; then A68: LIN o,b1,b3 by AFF_1:def_1; assume A69: a1 = a3 ; ::_thesis: a3,a4 // b3,b4 then a2,a1 // b2,b3 by A20, AFF_1:4; then b2,b1 // b2,b3 by A6, A15, A21, AFF_1:5; hence a3,a4 // b3,b4 by A3, A4, A5, A12, A16, A19, A22, A69, A68, AFF_1:14, AFF_1:25; ::_thesis: verum end; assume ( a1 = a3 or a2 = a4 ) ; ::_thesis: a3,a4 // b3,b4 hence a3,a4 // b3,b4 by A67, A64; ::_thesis: verum end; hence a3,a4 // b3,b4 by A23; ::_thesis: verum end; hence X is satisfying_major_Scherungssatz by Def2; ::_thesis: verum end; theorem :: CONMETR1:8 for X being AffinPlane holds ( X is Desarguesian iff X is satisfying_Scherungssatz ) proof let X be AffinPlane; ::_thesis: ( X is Desarguesian iff X is satisfying_Scherungssatz ) A1: ( X is satisfying_Scherungssatz implies X is Desarguesian ) proof assume A2: X is satisfying_Scherungssatz ; ::_thesis: X is Desarguesian now__::_thesis:_for_Y,_Z,_M_being_Subset_of_X for_o,_a,_b,_c,_a1,_b1,_c1_being_Element_of_X_st_o_in_Y_&_o_in_Z_&_o_in_M_&_o_<>_a_&_o_<>_b_&_o_<>_c_&_a_in_Y_&_a1_in_Y_&_b_in_Z_&_b1_in_Z_&_c_in_M_&_c1_in_M_&_Y_is_being_line_&_Z_is_being_line_&_M_is_being_line_&_Y_<>_Z_&_Y_<>_M_&_a,b_//_a1,b1_&_a,c_//_a1,c1_holds_ b,c_//_b1,c1 let Y, Z, M be Subset of X; ::_thesis: for o, a, b, c, a1, b1, c1 being Element of X st o in Y & o in Z & o in M & o <> a & o <> b & o <> c & a in Y & a1 in Y & b in Z & b1 in Z & c in M & c1 in M & Y is being_line & Z is being_line & M is being_line & Y <> Z & Y <> M & a,b // a1,b1 & a,c // a1,c1 holds b,c // b1,c1 let o, a, b, c, a1, b1, c1 be Element of X; ::_thesis: ( o in Y & o in Z & o in M & o <> a & o <> b & o <> c & a in Y & a1 in Y & b in Z & b1 in Z & c in M & c1 in M & Y is being_line & Z is being_line & M is being_line & Y <> Z & Y <> M & a,b // a1,b1 & a,c // a1,c1 implies b,c // b1,c1 ) assume that A3: o in Y and A4: o in Z and A5: o in M and A6: o <> a and A7: o <> b and A8: o <> c and A9: a in Y and A10: a1 in Y and A11: b in Z and A12: b1 in Z and A13: c in M and A14: c1 in M and A15: Y is being_line and A16: Z is being_line and A17: M is being_line and A18: Y <> Z and A19: Y <> M and A20: a,b // a1,b1 and A21: a,c // a1,c1 ; ::_thesis: b,c // b1,c1 assume A22: not b,c // b1,c1 ; ::_thesis: contradiction A23: now__::_thesis:_for_Y,_Z,_M_being_Subset_of_X for_o,_a,_b,_c,_a1,_b1,_c1,_d_being_Element_of_X_st_X_is_satisfying_Scherungssatz_&_o_in_Y_&_o_in_Z_&_o_in_M_&_o_<>_a_&_o_<>_b_&_o_<>_c_&_a_in_Y_&_a1_in_Y_&_b_in_Z_&_b1_in_Z_&_c_in_M_&_c1_in_M_&_Y_is_being_line_&_Z_is_being_line_&_M_is_being_line_&_Y_<>_Z_&_Y_<>_M_&_a,b_//_a1,b1_&_a,c_//_a1,c1_&_LIN_b,c,d_&_LIN_b1,c1,d_&_not_LIN_a,a1,d_holds_ b,c_//_b1,c1 let Y, Z, M be Subset of X; ::_thesis: for o, a, b, c, a1, b1, c1, d being Element of X st X is satisfying_Scherungssatz & o in Y & o in Z & o in M & o <> a & o <> b & o <> c & a in Y & a1 in Y & b in Z & b1 in Z & c in M & c1 in M & Y is being_line & Z is being_line & M is being_line & Y <> Z & Y <> M & a,b // a1,b1 & a,c // a1,c1 & LIN b,c,d & LIN b1,c1,d & not LIN a,a1,d holds b,c // b1,c1 let o, a, b, c, a1, b1, c1, d be Element of X; ::_thesis: ( X is satisfying_Scherungssatz & o in Y & o in Z & o in M & o <> a & o <> b & o <> c & a in Y & a1 in Y & b in Z & b1 in Z & c in M & c1 in M & Y is being_line & Z is being_line & M is being_line & Y <> Z & Y <> M & a,b // a1,b1 & a,c // a1,c1 & LIN b,c,d & LIN b1,c1,d & not LIN a,a1,d implies b,c // b1,c1 ) assume A24: X is satisfying_Scherungssatz ; ::_thesis: ( o in Y & o in Z & o in M & o <> a & o <> b & o <> c & a in Y & a1 in Y & b in Z & b1 in Z & c in M & c1 in M & Y is being_line & Z is being_line & M is being_line & Y <> Z & Y <> M & a,b // a1,b1 & a,c // a1,c1 & LIN b,c,d & LIN b1,c1,d & not LIN a,a1,d implies b,c // b1,c1 ) assume that A25: o in Y and A26: o in Z and A27: o in M and A28: o <> a and A29: o <> b and A30: o <> c and A31: a in Y and A32: a1 in Y and A33: b in Z and A34: b1 in Z and A35: c in M and A36: c1 in M and A37: Y is being_line and A38: Z is being_line and A39: M is being_line and A40: Y <> Z and A41: Y <> M and A42: a,b // a1,b1 and A43: a,c // a1,c1 and A44: LIN b,c,d and A45: LIN b1,c1,d ; ::_thesis: ( LIN a,a1,d or b,c // b1,c1 ) ( LIN a,a1,d or b,c // b1,c1 ) proof assume that A46: not LIN a,a1,d and A47: not b,c // b1,c1 ; ::_thesis: contradiction A48: ( c <> c1 & a <> a1 & b <> b1 ) proof A49: now__::_thesis:_not_b_=_b1 A50: not LIN o,a,c proof assume LIN o,a,c ; ::_thesis: contradiction then c in Y by A25, A28, A31, A37, AFF_1:25; then A51: o,c // Y by A25, A37, AFF_1:52; o,c // M by A27, A35, A39, AFF_1:52; hence contradiction by A25, A27, A30, A41, A51, AFF_1:45, AFF_1:53; ::_thesis: verum end; o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41; then A52: LIN o,c,c1 by AFF_1:def_1; A53: not LIN o,b,a proof assume LIN o,b,a ; ::_thesis: contradiction then a in Z by A26, A29, A33, A38, AFF_1:25; then A54: o,a // Z by A26, A38, AFF_1:52; o,a // Y by A25, A31, A37, AFF_1:52; hence contradiction by A25, A26, A28, A40, A54, AFF_1:45, AFF_1:53; ::_thesis: verum end; o,a // o,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41; then A55: LIN o,a,a1 by AFF_1:def_1; assume A56: b = b1 ; ::_thesis: contradiction then b,a // b,a1 by A42, AFF_1:4; then a = a1 by A53, A55, AFF_1:14; then c = c1 by A43, A50, A52, AFF_1:14; hence contradiction by A47, A56, AFF_1:2; ::_thesis: verum end; A57: now__::_thesis:_not_c_=_c1 A58: not LIN o,a,b proof assume LIN o,a,b ; ::_thesis: contradiction then b in Y by A25, A28, A31, A37, AFF_1:25; then A59: o,b // Y by A25, A37, AFF_1:52; o,b // Z by A26, A33, A38, AFF_1:52; hence contradiction by A25, A26, A29, A40, A59, AFF_1:45, AFF_1:53; ::_thesis: verum end; o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41; then A60: LIN o,b,b1 by AFF_1:def_1; A61: not LIN o,c,a proof assume LIN o,c,a ; ::_thesis: contradiction then a in M by A27, A30, A35, A39, AFF_1:25; then A62: o,a // M by A27, A39, AFF_1:52; o,a // Y by A25, A31, A37, AFF_1:52; hence contradiction by A25, A27, A28, A41, A62, AFF_1:45, AFF_1:53; ::_thesis: verum end; o,a // o,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41; then A63: LIN o,a,a1 by AFF_1:def_1; assume A64: c = c1 ; ::_thesis: contradiction then c,a // c,a1 by A43, AFF_1:4; then a = a1 by A61, A63, AFF_1:14; then b = b1 by A42, A58, A60, AFF_1:14; hence contradiction by A47, A64, AFF_1:2; ::_thesis: verum end; A65: now__::_thesis:_not_a_=_a1 A66: not LIN o,a,c proof assume LIN o,a,c ; ::_thesis: contradiction then c in Y by A25, A28, A31, A37, AFF_1:25; then A67: o,c // Y by A25, A37, AFF_1:52; o,c // M by A27, A35, A39, AFF_1:52; hence contradiction by A25, A27, A30, A41, A67, AFF_1:45, AFF_1:53; ::_thesis: verum end; A68: not LIN o,a,b proof assume LIN o,a,b ; ::_thesis: contradiction then b in Y by A25, A28, A31, A37, AFF_1:25; then A69: o,b // Y by A25, A37, AFF_1:52; o,b // Z by A26, A33, A38, AFF_1:52; hence contradiction by A25, A26, A29, A40, A69, AFF_1:45, AFF_1:53; ::_thesis: verum end; assume A70: a = a1 ; ::_thesis: contradiction o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41; then LIN o,c,c1 by AFF_1:def_1; then A71: c = c1 by A43, A70, A66, AFF_1:14; o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41; then LIN o,b,b1 by AFF_1:def_1; then b = b1 by A42, A70, A68, AFF_1:14; hence contradiction by A47, A71, AFF_1:2; ::_thesis: verum end; assume ( not c <> c1 or not a <> a1 or not b <> b1 ) ; ::_thesis: contradiction hence contradiction by A57, A65, A49; ::_thesis: verum end; now__::_thesis:_not_b_<>_c assume A72: b <> c ; ::_thesis: contradiction A73: now__::_thesis:_not_b1_<>_o assume A74: b1 <> o ; ::_thesis: contradiction A75: ( a1 <> b1 & a1 <> c1 ) proof A76: now__::_thesis:_not_a1_=_c1 A77: o <> a1 proof A78: not LIN a,b,o proof assume LIN a,b,o ; ::_thesis: contradiction then LIN o,a,b by AFF_1:6; then b in Y by A25, A28, A31, A37, AFF_1:25; then A79: o,b // Y by A25, A37, AFF_1:52; o,b // Z by A26, A33, A38, AFF_1:52; hence contradiction by A25, A26, A29, A40, A79, AFF_1:45, AFF_1:53; ::_thesis: verum end; A80: o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41; assume o = a1 ; ::_thesis: contradiction then a,b // o,b by A42, A74, A80, AFF_1:5; then b,a // b,o by AFF_1:4; then LIN b,a,o by AFF_1:def_1; then LIN o,a,b by AFF_1:6; then o,a // o,b by AFF_1:def_1; then o,a // o,b1 by A29, A80, AFF_1:5; then LIN o,a,b1 by AFF_1:def_1; then A81: LIN a,o,b1 by AFF_1:6; b,o // b,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41; hence contradiction by A74, A78, A81, AFF_1:14; ::_thesis: verum end; assume a1 = c1 ; ::_thesis: contradiction then A82: o,a1 // M by A27, A36, A39, AFF_1:52; o,a1 // Y by A25, A32, A37, AFF_1:52; hence contradiction by A25, A27, A41, A82, A77, AFF_1:45, AFF_1:53; ::_thesis: verum end; A83: now__::_thesis:_not_a1_=_b1 assume a1 = b1 ; ::_thesis: contradiction then A84: o,b1 // Y by A25, A32, A37, AFF_1:52; o,b1 // Z by A26, A34, A38, AFF_1:52; hence contradiction by A25, A26, A40, A74, A84, AFF_1:45, AFF_1:53; ::_thesis: verum end; assume ( not a1 <> b1 or not a1 <> c1 ) ; ::_thesis: contradiction hence contradiction by A83, A76; ::_thesis: verum end; LIN o,o,a by AFF_1:7; then consider C being Subset of X such that A85: C is being_line and A86: o in C and o in C and A87: a in C by AFF_1:21; A88: ex d2 being Element of X st ( d2 in C & a,c // d,d2 ) proof consider e2 being Element of X such that A89: a,c // d,e2 and A90: d <> e2 by DIRAF:40; consider e1 being Element of X such that A91: o,a // o,e1 and A92: o <> e1 by DIRAF:40; LIN o,a,e1 by A91, AFF_1:def_1; then A93: e1 in C by A28, A85, A86, A87, AFF_1:25; not o,e1 // d,e2 proof assume o,e1 // d,e2 ; ::_thesis: contradiction then o,a // d,e2 by A91, A92, AFF_1:5; then o,a // a,c by A89, A90, AFF_1:5; then a,o // a,c by AFF_1:4; then LIN a,o,c by AFF_1:def_1; then c in Y by A25, A28, A31, A37, AFF_1:25; then A94: o,c // Y by A25, A37, AFF_1:52; o,c // M by A27, A35, A39, AFF_1:52; hence contradiction by A25, A27, A30, A41, A94, AFF_1:45, AFF_1:53; ::_thesis: verum end; then consider d2 being Element of X such that A95: LIN o,e1,d2 and A96: LIN d,e2,d2 by AFF_1:60; take d2 ; ::_thesis: ( d2 in C & a,c // d,d2 ) d,e2 // d,d2 by A96, AFF_1:def_1; hence ( d2 in C & a,c // d,d2 ) by A85, A86, A92, A89, A90, A95, A93, AFF_1:5, AFF_1:25; ::_thesis: verum end; A97: ex d1 being Element of X st ( d1 in C & c,c1 // d,d1 ) proof consider e2 being Element of X such that A98: c,c1 // d,e2 and A99: d <> e2 by DIRAF:40; consider e1 being Element of X such that A100: o,a // o,e1 and A101: o <> e1 by DIRAF:40; LIN o,a,e1 by A100, AFF_1:def_1; then A102: e1 in C by A28, A85, A86, A87, AFF_1:25; not o,e1 // d,e2 proof assume o,e1 // d,e2 ; ::_thesis: contradiction then o,a // d,e2 by A100, A101, AFF_1:5; then A103: o,a // c,c1 by A98, A99, AFF_1:5; c,c1 // o,c by A27, A35, A36, A39, AFF_1:39, AFF_1:41; then o,a // o,c by A48, A103, AFF_1:5; then LIN o,a,c by AFF_1:def_1; then c in Y by A25, A28, A31, A37, AFF_1:25; then A104: o,c // Y by A25, A37, AFF_1:52; o,c // M by A27, A35, A39, AFF_1:52; hence contradiction by A25, A27, A30, A41, A104, AFF_1:45, AFF_1:53; ::_thesis: verum end; then consider d1 being Element of X such that A105: LIN o,e1,d1 and A106: LIN d,e2,d1 by AFF_1:60; take d1 ; ::_thesis: ( d1 in C & c,c1 // d,d1 ) d,e2 // d,d1 by A106, AFF_1:def_1; hence ( d1 in C & c,c1 // d,d1 ) by A85, A86, A101, A98, A99, A105, A102, AFF_1:5, AFF_1:25; ::_thesis: verum end; consider d2 being Element of X such that A107: d2 in C and A108: a,c // d,d2 by A88; consider d1 being Element of X such that A109: d1 in C and A110: c,c1 // d,d1 by A97; c,c1 // c,o by A27, A35, A36, A39, AFF_1:39, AFF_1:41; then A111: c,o // d,d1 by A48, A110, AFF_1:5; o,a // o,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41; then LIN o,a,a1 by AFF_1:def_1; then A112: a1 in C by A28, A85, A86, A87, AFF_1:25; LIN b,b,c by AFF_1:7; then consider A being Subset of X such that A113: A is being_line and A114: b in A and b in A and A115: c in A by AFF_1:21; A116: d in A by A44, A72, A113, A114, A115, AFF_1:25; A117: b <> c by A47, AFF_1:3; A118: ex d3 being Element of X st ( d3 in A & o,b // d1,d3 ) proof consider e2 being Element of X such that A119: o,b // d1,e2 and A120: d1 <> e2 by DIRAF:40; consider e1 being Element of X such that A121: b,c // b,e1 and A122: b <> e1 by DIRAF:40; LIN b,c,e1 by A121, AFF_1:def_1; then A123: e1 in A by A117, A113, A114, A115, AFF_1:25; not b,e1 // d1,e2 proof assume b,e1 // d1,e2 ; ::_thesis: contradiction then b,c // d1,e2 by A121, A122, AFF_1:5; then A124: b,c // o,b by A119, A120, AFF_1:5; then b,c // b,o by AFF_1:4; then LIN b,c,o by AFF_1:def_1; then LIN o,b,c by AFF_1:6; then A125: o,b // o,c by AFF_1:def_1; A126: o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41; o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41; then o,b // o,c1 by A30, A125, AFF_1:5; then o,b1 // o,c1 by A29, A126, AFF_1:5; then LIN o,b1,c1 by AFF_1:def_1; then LIN b1,c1,o by AFF_1:6; then b1,c1 // b1,o by AFF_1:def_1; then b1,c1 // o,b1 by AFF_1:4; then b1,c1 // o,b by A74, A126, AFF_1:5; hence contradiction by A29, A47, A124, AFF_1:5; ::_thesis: verum end; then consider d3 being Element of X such that A127: LIN b,e1,d3 and A128: LIN d1,e2,d3 by AFF_1:60; take d3 ; ::_thesis: ( d3 in A & o,b // d1,d3 ) d1,e2 // d1,d3 by A128, AFF_1:def_1; hence ( d3 in A & o,b // d1,d3 ) by A113, A114, A122, A119, A120, A127, A123, AFF_1:5, AFF_1:25; ::_thesis: verum end; A129: ( not o in A & not a in A & not d1 in A & not d2 in A ) proof A130: now__::_thesis:_not_a_in_A A131: a <> b proof assume a = b ; ::_thesis: contradiction then A132: o,b // Y by A25, A31, A37, AFF_1:52; o,b // Z by A26, A33, A38, AFF_1:52; hence contradiction by A25, A26, A29, A40, A132, AFF_1:45, AFF_1:53; ::_thesis: verum end; A133: a1 <> b1 proof assume a1 = b1 ; ::_thesis: contradiction then A134: o,b1 // Y by A25, A32, A37, AFF_1:52; o,b1 // Z by A26, A34, A38, AFF_1:52; hence contradiction by A25, A26, A40, A74, A134, AFF_1:45, AFF_1:53; ::_thesis: verum end; assume a in A ; ::_thesis: contradiction then A135: a,b // a,c by A113, A114, A115, AFF_1:39, AFF_1:41; a <> c proof assume a = c ; ::_thesis: contradiction then A136: o,c // Y by A25, A31, A37, AFF_1:52; o,c // M by A27, A35, A39, AFF_1:52; hence contradiction by A25, A27, A30, A41, A136, AFF_1:45, AFF_1:53; ::_thesis: verum end; then a,b // a1,c1 by A43, A135, AFF_1:5; then a1,b1 // a1,c1 by A42, A131, AFF_1:5; then LIN a1,b1,c1 by AFF_1:def_1; then LIN b1,c1,a1 by AFF_1:6; then b1,c1 // b1,a1 by AFF_1:def_1; then A137: a1,b1 // b1,c1 by AFF_1:4; LIN a,b,c by A135, AFF_1:def_1; then LIN b,c,a by AFF_1:6; then b,c // b,a by AFF_1:def_1; then b,c // a,b by AFF_1:4; then b,c // a1,b1 by A42, A131, AFF_1:5; hence contradiction by A47, A137, A133, AFF_1:5; ::_thesis: verum end; A138: now__::_thesis:_not_d2_in_A A139: d <> d2 proof o,a // o,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41; then LIN o,a,a1 by AFF_1:def_1; then A140: a1 in C by A28, A85, A86, A87, AFF_1:25; assume d = d2 ; ::_thesis: contradiction then a,a1 // a,d by A85, A87, A107, A140, AFF_1:39, AFF_1:41; hence contradiction by A46, AFF_1:def_1; ::_thesis: verum end; assume A141: d2 in A ; ::_thesis: contradiction A142: d,d2 // c,a by A108, AFF_1:4; d in A by A44, A117, A113, A114, A115, AFF_1:25; hence contradiction by A113, A115, A130, A141, A139, A142, AFF_1:48; ::_thesis: verum end; A143: now__::_thesis:_not_o_in_A assume o in A ; ::_thesis: contradiction then A144: o,b // o,c by A113, A114, A115, AFF_1:39, AFF_1:41; A145: o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41; o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41; then o,b // o,c1 by A30, A144, AFF_1:5; then o,b1 // o,c1 by A29, A145, AFF_1:5; then LIN o,b1,c1 by AFF_1:def_1; then LIN b1,c1,o by AFF_1:6; then b1,c1 // b1,o by AFF_1:def_1; then b1,c1 // o,b1 by AFF_1:4; then o,b // b1,c1 by A74, A145, AFF_1:5; then A146: b,o // b1,c1 by AFF_1:4; LIN o,b,c by A144, AFF_1:def_1; then LIN b,c,o by AFF_1:6; then b,c // b,o by AFF_1:def_1; hence contradiction by A29, A47, A146, AFF_1:5; ::_thesis: verum end; A147: now__::_thesis:_not_d1_in_A A148: d <> d1 proof o,a // o,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41; then LIN o,a,a1 by AFF_1:def_1; then A149: a1 in C by A28, A85, A86, A87, AFF_1:25; assume d = d1 ; ::_thesis: contradiction then a,a1 // a,d by A85, A87, A109, A149, AFF_1:39, AFF_1:41; hence contradiction by A46, AFF_1:def_1; ::_thesis: verum end; assume A150: d1 in A ; ::_thesis: contradiction c,c1 // c,o by A27, A35, A36, A39, AFF_1:39, AFF_1:41; then A151: LIN c,c1,o by AFF_1:def_1; A152: d,d1 // c,c1 by A110, AFF_1:4; d in A by A44, A117, A113, A114, A115, AFF_1:25; then c1 in A by A113, A115, A150, A148, A152, AFF_1:48; hence contradiction by A48, A113, A115, A143, A151, AFF_1:25; ::_thesis: verum end; assume ( o in A or a in A or d1 in A or d2 in A ) ; ::_thesis: contradiction hence contradiction by A143, A130, A147, A138; ::_thesis: verum end; LIN b1,b1,c1 by AFF_1:7; then consider K being Subset of X such that A153: K is being_line and A154: b1 in K and b1 in K and A155: c1 in K by AFF_1:21; b1 <> c1 by A47, AFF_1:3; then A156: d in K by A45, A153, A154, A155, AFF_1:25; consider d3 being Element of X such that A157: d3 in A and A158: o,b // d1,d3 by A118; A159: b1 <> c1 by A47, AFF_1:3; ex d4 being Element of X st ( d4 in K & d1,d3 // d1,d4 ) proof consider e2 being Element of X such that A160: d1,d3 // d1,e2 and A161: d1 <> e2 by DIRAF:40; consider e1 being Element of X such that A162: b1,c1 // b1,e1 and A163: b1 <> e1 by DIRAF:40; LIN b1,c1,e1 by A162, AFF_1:def_1; then A164: e1 in K by A159, A153, A154, A155, AFF_1:25; not b1,e1 // d1,e2 proof A165: o <> c1 proof A166: not LIN a,c,o proof assume LIN a,c,o ; ::_thesis: contradiction then LIN o,a,c by AFF_1:6; then c in Y by A25, A28, A31, A37, AFF_1:25; then A167: o,c // Y by A25, A37, AFF_1:52; o,c // M by A27, A35, A39, AFF_1:52; hence contradiction by A25, A27, A30, A41, A167, AFF_1:45, AFF_1:53; ::_thesis: verum end; assume A168: o = c1 ; ::_thesis: contradiction a1,o // a,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41; then a,c // a,a1 by A43, A75, A168, AFF_1:5; then LIN a,c,a1 by AFF_1:def_1; then LIN a1,c,a by AFF_1:6; then A169: a1,c // a1,a by AFF_1:def_1; a1,a // a1,o by A25, A31, A32, A37, AFF_1:39, AFF_1:41; then a1,c // a1,o by A48, A169, AFF_1:5; then LIN a1,c,o by AFF_1:def_1; then LIN c,o,a1 by AFF_1:6; then A170: c,o // c,a1 by AFF_1:def_1; a,o // a,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41; then LIN a,o,a1 by AFF_1:def_1; hence contradiction by A75, A168, A166, A170, AFF_1:14; ::_thesis: verum end; A171: d1 <> d3 proof A172: d <> d1 proof o,a // o,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41; then LIN o,a,a1 by AFF_1:def_1; then A173: a1 in C by A28, A85, A86, A87, AFF_1:25; assume d = d1 ; ::_thesis: contradiction then a,a1 // a,d by A85, A87, A109, A173, AFF_1:39, AFF_1:41; hence contradiction by A46, AFF_1:def_1; ::_thesis: verum end; assume A174: d1 = d3 ; ::_thesis: contradiction c,c1 // o,c by A27, A35, A36, A39, AFF_1:39, AFF_1:41; then o,c // d,d1 by A48, A110, AFF_1:5; then A175: d,d1 // c,o by AFF_1:4; A176: o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41; d in A by A44, A117, A113, A114, A115, AFF_1:25; then o in A by A113, A115, A157, A174, A172, A175, AFF_1:48; then A177: o,b // o,c by A113, A114, A115, AFF_1:39, AFF_1:41; o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41; then o,b // o,c1 by A30, A177, AFF_1:5; then o,b1 // o,c1 by A29, A176, AFF_1:5; then LIN o,b1,c1 by AFF_1:def_1; then LIN b1,c1,o by AFF_1:6; then b1,c1 // b1,o by AFF_1:def_1; then b1,c1 // o,b1 by AFF_1:4; then A178: o,b // b1,c1 by A74, A176, AFF_1:5; LIN o,b,c by A177, AFF_1:def_1; then LIN b,c,o by AFF_1:6; then b,c // b,o by AFF_1:def_1; then b,c // o,b by AFF_1:4; hence contradiction by A29, A47, A178, AFF_1:5; ::_thesis: verum end; assume b1,e1 // d1,e2 ; ::_thesis: contradiction then b1,c1 // d1,e2 by A162, A163, AFF_1:5; then A179: b1,c1 // d1,d3 by A160, A161, AFF_1:5; A180: o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41; then o,b1 // d1,d3 by A29, A158, AFF_1:5; then A181: o,b1 // b1,c1 by A179, A171, AFF_1:5; then b1,o // b1,c1 by AFF_1:4; then LIN b1,o,c1 by AFF_1:def_1; then LIN o,b1,c1 by AFF_1:6; then o,b1 // o,c1 by AFF_1:def_1; then A182: o,b // o,c1 by A74, A180, AFF_1:5; o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41; then o,b // o,c by A182, A165, AFF_1:5; then LIN o,b,c by AFF_1:def_1; then LIN b,o,c by AFF_1:6; then b,o // b,c by AFF_1:def_1; then o,b // b,c by AFF_1:4; then o,b1 // b,c by A29, A180, AFF_1:5; hence contradiction by A47, A74, A181, AFF_1:5; ::_thesis: verum end; then consider d4 being Element of X such that A183: LIN b1,e1,d4 and A184: LIN d1,e2,d4 by AFF_1:60; take d4 ; ::_thesis: ( d4 in K & d1,d3 // d1,d4 ) d1,e2 // d1,d4 by A184, AFF_1:def_1; hence ( d4 in K & d1,d3 // d1,d4 ) by A153, A154, A163, A160, A161, A183, A164, AFF_1:5, AFF_1:25; ::_thesis: verum end; then consider d4 being Element of X such that A185: d4 in K and A186: d1,d3 // d1,d4 ; A187: ( not c in C & not b in C & not d in C & not d3 in C ) proof A188: now__::_thesis:_not_b_in_C assume b in C ; ::_thesis: contradiction then o,a // o,b by A85, A86, A87, AFF_1:39, AFF_1:41; then LIN o,a,b by AFF_1:def_1; then b in Y by A25, A28, A31, A37, AFF_1:25; then A189: o,b // Y by A25, A37, AFF_1:52; o,b // Z by A26, A33, A38, AFF_1:52; hence contradiction by A25, A26, A29, A40, A189, AFF_1:45, AFF_1:53; ::_thesis: verum end; A190: now__::_thesis:_not_d3_in_C A191: d1 <> d3 proof A192: d <> d1 proof o,a // o,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41; then LIN o,a,a1 by AFF_1:def_1; then A193: a1 in C by A28, A85, A86, A87, AFF_1:25; assume d = d1 ; ::_thesis: contradiction then a,a1 // a,d by A85, A87, A109, A193, AFF_1:39, AFF_1:41; hence contradiction by A46, AFF_1:def_1; ::_thesis: verum end; assume A194: d1 = d3 ; ::_thesis: contradiction A195: o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41; A196: d,d1 // c,c1 by A110, AFF_1:4; d in A by A44, A117, A113, A114, A115, AFF_1:25; then c1 in A by A113, A115, A157, A194, A192, A196, AFF_1:48; then A197: c,c1 // c,b by A113, A114, A115, AFF_1:39, AFF_1:41; A198: o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41; c,o // c,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41; then c,o // c,b by A48, A197, AFF_1:5; then A199: LIN c,o,b by AFF_1:def_1; then LIN o,b,c by AFF_1:6; then o,b // o,c by AFF_1:def_1; then o,b1 // o,c by A29, A198, AFF_1:5; then o,b1 // o,c1 by A30, A195, AFF_1:5; then LIN o,b1,c1 by AFF_1:def_1; then LIN b1,c1,o by AFF_1:6; then b1,c1 // b1,o by AFF_1:def_1; then b1,c1 // o,b1 by AFF_1:4; then A200: o,b // b1,c1 by A74, A198, AFF_1:5; LIN b,c,o by A199, AFF_1:6; then b,c // b,o by AFF_1:def_1; then b,c // o,b by AFF_1:4; hence contradiction by A29, A47, A200, AFF_1:5; ::_thesis: verum end; assume A201: d3 in C ; ::_thesis: contradiction d1,d3 // o,b by A158, AFF_1:4; hence contradiction by A85, A86, A109, A188, A201, A191, AFF_1:48; ::_thesis: verum end; A202: now__::_thesis:_not_c_in_C assume c in C ; ::_thesis: contradiction then o,a // o,c by A85, A86, A87, AFF_1:39, AFF_1:41; then LIN o,a,c by AFF_1:def_1; then c in Y by A25, A28, A31, A37, AFF_1:25; then A203: o,c // Y by A25, A37, AFF_1:52; o,c // M by A27, A35, A39, AFF_1:52; hence contradiction by A25, A27, A30, A41, A203, AFF_1:45, AFF_1:53; ::_thesis: verum end; A204: now__::_thesis:_not_d_in_C assume d in C ; ::_thesis: contradiction then A205: o,a // a,d by A85, A86, A87, AFF_1:39, AFF_1:41; o,a // a,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41; then a,a1 // a,d by A28, A205, AFF_1:5; hence contradiction by A46, AFF_1:def_1; ::_thesis: verum end; assume ( c in C or b in C or d in C or d3 in C ) ; ::_thesis: contradiction hence contradiction by A202, A188, A204, A190; ::_thesis: verum end; A206: d4 <> d3 proof assume A207: d4 = d3 ; ::_thesis: contradiction d = d3 proof d in A by A44, A117, A113, A114, A115, AFF_1:25; then A208: b,c // d,d3 by A113, A114, A115, A157, AFF_1:39, AFF_1:41; d in K by A45, A159, A153, A154, A155, AFF_1:25; then A209: b1,c1 // d,d3 by A153, A154, A155, A185, A207, AFF_1:39, AFF_1:41; assume d <> d3 ; ::_thesis: contradiction hence contradiction by A47, A209, A208, AFF_1:5; ::_thesis: verum end; then A210: o,b // d,d1 by A158, AFF_1:4; o,c // c,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41; then o,c // d,d1 by A48, A110, AFF_1:5; then A211: o,b // o,c by A109, A187, A210, AFF_1:5; A212: o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41; A213: o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41; then o,b1 // o,c by A29, A211, AFF_1:5; then o,b1 // o,c1 by A30, A212, AFF_1:5; then LIN o,b1,c1 by AFF_1:def_1; then LIN b1,c1,o by AFF_1:6; then b1,c1 // b1,o by AFF_1:def_1; then b1,c1 // o,b1 by AFF_1:4; then A214: o,b // b1,c1 by A74, A213, AFF_1:5; LIN o,b,c by A211, AFF_1:def_1; then LIN b,c,o by AFF_1:6; then b,c // b,o by AFF_1:def_1; then b,c // o,b by AFF_1:4; hence contradiction by A29, A47, A214, AFF_1:5; ::_thesis: verum end; A215: ( a <> b & a <> c ) proof A216: now__::_thesis:_not_a_=_c assume a = c ; ::_thesis: contradiction then A217: o,a // M by A27, A35, A39, AFF_1:52; o,a // Y by A25, A31, A37, AFF_1:52; hence contradiction by A25, A27, A28, A41, A217, AFF_1:45, AFF_1:53; ::_thesis: verum end; A218: now__::_thesis:_not_a_=_b assume a = b ; ::_thesis: contradiction then A219: o,a // Z by A26, A33, A38, AFF_1:52; o,a // Y by A25, A31, A37, AFF_1:52; hence contradiction by A25, A26, A28, A40, A219, AFF_1:45, AFF_1:53; ::_thesis: verum end; assume ( not a <> b or not a <> c ) ; ::_thesis: contradiction hence contradiction by A218, A216; ::_thesis: verum end; A220: ( not o in K & not a1 in K & not d1 in K & not d2 in K ) proof A221: now__::_thesis:_not_o_in_K A222: o <> c1 proof A223: a1 <> o proof A224: not LIN a,b,o proof assume LIN a,b,o ; ::_thesis: contradiction then LIN o,a,b by AFF_1:6; then b in Y by A25, A28, A31, A37, AFF_1:25; then A225: o,b // Y by A25, A37, AFF_1:52; o,b // Z by A26, A33, A38, AFF_1:52; hence contradiction by A25, A26, A29, A40, A225, AFF_1:45, AFF_1:53; ::_thesis: verum end; A226: o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41; assume a1 = o ; ::_thesis: contradiction then a,b // o,b by A42, A74, A226, AFF_1:5; then b,a // b,o by AFF_1:4; then LIN b,a,o by AFF_1:def_1; then LIN o,a,b by AFF_1:6; then o,a // o,b by AFF_1:def_1; then o,a // o,b1 by A29, A226, AFF_1:5; then LIN o,a,b1 by AFF_1:def_1; then A227: LIN a,o,b1 by AFF_1:6; b,o // b,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41; hence contradiction by A74, A224, A227, AFF_1:14; ::_thesis: verum end; A228: not LIN c,a,o proof assume LIN c,a,o ; ::_thesis: contradiction then LIN o,a,c by AFF_1:6; then c in Y by A25, A28, A31, A37, AFF_1:25; then A229: o,c // Y by A25, A37, AFF_1:52; o,c // M by A27, A35, A39, AFF_1:52; hence contradiction by A25, A27, A30, A41, A229, AFF_1:45, AFF_1:53; ::_thesis: verum end; A230: a1,o // o,a by A25, A31, A32, A37, AFF_1:39, AFF_1:41; assume o = c1 ; ::_thesis: contradiction then a,c // o,a by A43, A223, A230, AFF_1:5; then a,c // a,o by AFF_1:4; then LIN a,c,o by AFF_1:def_1; then LIN o,c,a by AFF_1:6; then o,c // o,a by AFF_1:def_1; then o,c // a1,o by A28, A230, AFF_1:5; then o,c // o,a1 by AFF_1:4; then LIN o,c,a1 by AFF_1:def_1; then A231: LIN c,o,a1 by AFF_1:6; a,o // a,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41; hence contradiction by A223, A228, A231, AFF_1:14; ::_thesis: verum end; A232: o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41; assume o in K ; ::_thesis: contradiction then A233: o,b1 // o,c1 by A153, A154, A155, AFF_1:39, AFF_1:41; A234: o,b1 // o,b by A26, A33, A34, A38, AFF_1:39, AFF_1:41; then o,b // o,c1 by A74, A233, AFF_1:5; then o,b // o,c by A222, A232, AFF_1:5; then LIN o,b,c by AFF_1:def_1; then LIN b,c,o by AFF_1:6; then b,c // b,o by AFF_1:def_1; then b,c // o,b by AFF_1:4; then b,c // o,b1 by A29, A234, AFF_1:5; then A235: b,c // b1,o by AFF_1:4; LIN o,b1,c1 by A233, AFF_1:def_1; then LIN b1,c1,o by AFF_1:6; then b1,c1 // b1,o by AFF_1:def_1; hence contradiction by A47, A74, A235, AFF_1:5; ::_thesis: verum end; A236: now__::_thesis:_not_d1_in_K A237: d <> d1 proof assume d = d1 ; ::_thesis: contradiction then A238: o,a // a,d by A85, A86, A87, A109, AFF_1:39, AFF_1:41; o,a // a,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41; then a,a1 // a,d by A28, A238, AFF_1:5; hence contradiction by A46, AFF_1:def_1; ::_thesis: verum end; assume A239: d1 in K ; ::_thesis: contradiction c,c1 // c,o by A27, A35, A36, A39, AFF_1:39, AFF_1:41; then A240: LIN c,c1,o by AFF_1:def_1; A241: d,d1 // c1,c by A110, AFF_1:4; d in K by A45, A159, A153, A154, A155, AFF_1:25; then c in K by A153, A155, A239, A237, A241, AFF_1:48; hence contradiction by A48, A153, A155, A221, A240, AFF_1:25; ::_thesis: verum end; A242: now__::_thesis:_not_a1_in_K assume a1 in K ; ::_thesis: contradiction then A243: a1,b1 // a1,c1 by A153, A154, A155, AFF_1:39, AFF_1:41; then a,b // a1,c1 by A42, A75, AFF_1:5; then a,b // a,c by A43, A75, AFF_1:5; then LIN a,b,c by AFF_1:def_1; then LIN b,c,a by AFF_1:6; then b,c // b,a by AFF_1:def_1; then b,c // a,b by AFF_1:4; then A244: b,c // a1,b1 by A42, A215, AFF_1:5; LIN a1,b1,c1 by A243, AFF_1:def_1; then LIN b1,c1,a1 by AFF_1:6; then b1,c1 // b1,a1 by AFF_1:def_1; then b1,c1 // a1,b1 by AFF_1:4; hence contradiction by A47, A75, A244, AFF_1:5; ::_thesis: verum end; A245: now__::_thesis:_not_d2_in_K A246: d <> d2 proof assume d = d2 ; ::_thesis: contradiction then A247: o,a // a,d by A85, A86, A87, A107, AFF_1:39, AFF_1:41; o,a // a,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41; then a,a1 // a,d by A28, A247, AFF_1:5; hence contradiction by A46, AFF_1:def_1; ::_thesis: verum end; assume A248: d2 in K ; ::_thesis: contradiction d,d2 // a1,c1 by A43, A215, A108, AFF_1:5; then A249: d,d2 // c1,a1 by AFF_1:4; d in K by A45, A159, A153, A154, A155, AFF_1:25; hence contradiction by A153, A155, A242, A248, A246, A249, AFF_1:48; ::_thesis: verum end; assume ( o in K or a1 in K or d1 in K or d2 in K ) ; ::_thesis: contradiction hence contradiction by A221, A242, A236, A245; ::_thesis: verum end; A250: ( not c1 in C & not b1 in C & not d in C & not d4 in C ) proof A251: now__::_thesis:_not_c1_in_C assume A252: c1 in C ; ::_thesis: contradiction o,c1 // c1,c by A27, A35, A36, A39, AFF_1:39, AFF_1:41; hence contradiction by A155, A85, A86, A187, A220, A252, AFF_1:48; ::_thesis: verum end; A253: now__::_thesis:_not_d4_in_C assume A254: d4 in C ; ::_thesis: contradiction d1,d4 // d1,d3 by A186, AFF_1:4; hence contradiction by A85, A109, A185, A187, A220, A254, AFF_1:48; ::_thesis: verum end; A255: now__::_thesis:_not_b1_in_C assume A256: b1 in C ; ::_thesis: contradiction o,b1 // o,b by A26, A33, A34, A38, AFF_1:39, AFF_1:41; hence contradiction by A74, A85, A86, A187, A256, AFF_1:48; ::_thesis: verum end; assume ( c1 in C or b1 in C or d in C or d4 in C ) ; ::_thesis: contradiction hence contradiction by A187, A251, A255, A253; ::_thesis: verum end; a <> c proof assume a = c ; ::_thesis: contradiction then A257: o,a // M by A27, A35, A39, AFF_1:52; o,a // Y by A25, A31, A37, AFF_1:52; hence contradiction by A25, A27, A28, A41, A257, AFF_1:45, AFF_1:53; ::_thesis: verum end; then a1,c1 // d,d2 by A43, A108, AFF_1:5; then A258: a1,c1 // d2,d by AFF_1:4; c1,o // c,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41; then A259: c1,o // d,d1 by A48, A110, AFF_1:5; A260: d1 <> d2 proof assume d1 = d2 ; ::_thesis: contradiction then a,c // c,c1 by A109, A110, A108, A187, AFF_1:5; then c,c1 // c,a by AFF_1:4; then LIN c,c1,a by AFF_1:def_1; then a in M by A35, A36, A39, A48, AFF_1:25; then A261: o,a // M by A27, A39, AFF_1:52; o,a // Y by A25, A31, A37, AFF_1:52; hence contradiction by A25, A27, A28, A41, A261, AFF_1:45, AFF_1:53; ::_thesis: verum end; A262: not LIN d4,d2,d1 proof assume LIN d4,d2,d1 ; ::_thesis: contradiction then LIN d1,d2,d4 by AFF_1:6; hence contradiction by A85, A109, A107, A250, A260, AFF_1:25; ::_thesis: verum end; A263: o,b // o,b1 by A26, A33, A34, A38, AFF_1:51; a,c // d2,d by A108, AFF_1:4; then a,b // d2,d3 by A24, A113, A114, A115, A85, A86, A87, A109, A107, A157, A158, A116, A129, A187, A111, Def3; then A264: d2,d3 // a1,b1 by A42, A215, AFF_1:5; o,b // d1,d4 by A109, A158, A186, A187, AFF_1:5; then o,b1 // d1,d4 by A29, A263, AFF_1:5; then a1,b1 // d2,d4 by A24, A153, A154, A155, A85, A86, A109, A107, A185, A112, A156, A220, A250, A258, A259, Def3; then d2,d3 // d2,d4 by A75, A264, AFF_1:5; then LIN d2,d3,d4 by AFF_1:def_1; then LIN d4,d3,d2 by AFF_1:6; then A265: d4,d3 // d4,d2 by AFF_1:def_1; LIN d1,d3,d4 by A186, AFF_1:def_1; then LIN d4,d3,d1 by AFF_1:6; then d4,d3 // d4,d1 by AFF_1:def_1; then d4,d2 // d4,d1 by A206, A265, AFF_1:5; hence contradiction by A262, AFF_1:def_1; ::_thesis: verum end; now__::_thesis:_not_b1_=_o assume A266: b1 = o ; ::_thesis: contradiction A267: o = a1 proof A268: not LIN b,a,o proof assume LIN b,a,o ; ::_thesis: contradiction then LIN o,a,b by AFF_1:6; then b in Y by A25, A28, A31, A37, AFF_1:25; then A269: o,b // Y by A25, A37, AFF_1:52; o,b // Z by A26, A33, A38, AFF_1:52; hence contradiction by A25, A26, A29, A40, A269, AFF_1:45, AFF_1:53; ::_thesis: verum end; A270: a1 <> a proof assume a1 = a ; ::_thesis: contradiction then LIN a,b,o by A42, A266, AFF_1:def_1; then LIN o,a,b by AFF_1:6; then b in Y by A25, A28, A31, A37, AFF_1:25; then A271: o,b // Y by A25, A37, AFF_1:52; o,b // Z by A26, A33, A38, AFF_1:52; hence contradiction by A25, A26, A29, A40, A271, AFF_1:45, AFF_1:53; ::_thesis: verum end; assume A272: o <> a1 ; ::_thesis: contradiction a1,o // a,a1 by A25, A31, A32, A37, AFF_1:51; then a,b // a,a1 by A42, A266, A272, AFF_1:5; then LIN a,b,a1 by AFF_1:def_1; then LIN a1,b,a by AFF_1:6; then A273: a1,b // a1,a by AFF_1:def_1; a1,a // a1,o by A25, A31, A32, A37, AFF_1:51; then a1,b // a1,o by A273, A270, AFF_1:5; then LIN a1,b,o by AFF_1:def_1; then LIN b,o,a1 by AFF_1:6; hence contradiction by A25, A31, A32, A37, A272, A268, AFF_1:14, AFF_1:51; ::_thesis: verum end; o = c1 proof A274: not LIN a,c,o proof assume LIN a,c,o ; ::_thesis: contradiction then LIN o,a,c by AFF_1:6; then c in Y by A25, A28, A31, A37, AFF_1:25; then A275: o,c // Y by A25, A37, AFF_1:52; o,c // M by A27, A35, A39, AFF_1:52; hence contradiction by A25, A27, A30, A41, A275, AFF_1:45, AFF_1:53; ::_thesis: verum end; assume A276: o <> c1 ; ::_thesis: contradiction A277: o,c1 // o,c by A27, A35, A36, A39, AFF_1:51; then o,c // a,c by A43, A267, A276, AFF_1:5; then c,o // c,a by AFF_1:4; then LIN c,o,a by AFF_1:def_1; then LIN o,a,c by AFF_1:6; then o,a // o,c by AFF_1:def_1; then o,a // o,c1 by A30, A277, AFF_1:5; then LIN o,a,c1 by AFF_1:def_1; then LIN a,o,c1 by AFF_1:6; hence contradiction by A27, A35, A36, A39, A276, A274, AFF_1:14, AFF_1:51; ::_thesis: verum end; hence contradiction by A47, A266, AFF_1:3; ::_thesis: verum end; hence contradiction by A73; ::_thesis: verum end; hence contradiction by A47, AFF_1:3; ::_thesis: verum end; hence ( LIN a,a1,d or b,c // b1,c1 ) ; ::_thesis: verum end; A278: now__::_thesis:_Z_//_M A279: M // M by A17, AFF_1:41; consider d being Element of X such that A280: LIN b,c,d and A281: LIN b1,c1,d by A22, AFF_1:60; A282: LIN a,a1,d by A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, A23, A280, A281; A283: ( not a in Z & not a in M ) proof A284: now__::_thesis:_not_a_in_M assume a in M ; ::_thesis: contradiction then A285: o,a // M by A5, A17, AFF_1:52; o,a // Y by A3, A9, A15, AFF_1:52; hence contradiction by A3, A5, A6, A19, A285, AFF_1:45, AFF_1:53; ::_thesis: verum end; A286: now__::_thesis:_not_a_in_Z assume a in Z ; ::_thesis: contradiction then A287: o,a // Z by A4, A16, AFF_1:52; o,a // Y by A3, A9, A15, AFF_1:52; hence contradiction by A3, A4, A6, A18, A287, AFF_1:45, AFF_1:53; ::_thesis: verum end; assume ( a in Z or a in M ) ; ::_thesis: contradiction hence contradiction by A286, A284; ::_thesis: verum end; A288: ex d1 being Element of X st ( a,b // d,d1 & d1 in Z ) proof consider e1 being Element of X such that A289: o,b // o,e1 and A290: o <> e1 by DIRAF:40; consider e2 being Element of X such that A291: a,b // d,e2 and A292: d <> e2 by DIRAF:40; not o,e1 // d,e2 proof assume o,e1 // d,e2 ; ::_thesis: contradiction then o,b // d,e2 by A289, A290, AFF_1:5; then o,b // a,b by A291, A292, AFF_1:5; then b,o // b,a by AFF_1:4; then LIN b,o,a by AFF_1:def_1; hence contradiction by A4, A7, A11, A16, A283, AFF_1:25; ::_thesis: verum end; then consider d1 being Element of X such that A293: LIN o,e1,d1 and A294: LIN d,e2,d1 by AFF_1:60; o,e1 // o,d1 by A293, AFF_1:def_1; then o,b // o,d1 by A289, A290, AFF_1:5; then A295: LIN o,b,d1 by AFF_1:def_1; take d1 ; ::_thesis: ( a,b // d,d1 & d1 in Z ) d,e2 // d,d1 by A294, AFF_1:def_1; hence ( a,b // d,d1 & d1 in Z ) by A4, A7, A11, A16, A291, A292, A295, AFF_1:5, AFF_1:25; ::_thesis: verum end; A296: Z // Z by A16, AFF_1:41; A297: ( a <> a1 & b <> b1 & c <> c1 ) proof A298: now__::_thesis:_not_a_=_a1 A299: not LIN a,o,b proof assume LIN a,o,b ; ::_thesis: contradiction then LIN o,b,a by AFF_1:6; hence contradiction by A4, A7, A11, A16, A283, AFF_1:25; ::_thesis: verum end; A300: not LIN a,o,c proof assume LIN a,o,c ; ::_thesis: contradiction then LIN o,c,a by AFF_1:6; hence contradiction by A5, A8, A13, A17, A283, AFF_1:25; ::_thesis: verum end; assume A301: a = a1 ; ::_thesis: contradiction then LIN a,c,c1 by A21, AFF_1:def_1; then A302: c = c1 by A5, A13, A14, A279, A300, AFF_1:14, AFF_1:39; LIN a,b,b1 by A20, A301, AFF_1:def_1; then b = b1 by A4, A11, A12, A296, A299, AFF_1:14, AFF_1:39; hence contradiction by A22, A302, AFF_1:2; ::_thesis: verum end; A303: now__::_thesis:_not_b_=_b1 assume b = b1 ; ::_thesis: contradiction then b,a // b,a1 by A20, AFF_1:4; then A304: LIN b,a,a1 by AFF_1:def_1; o,a // o,a1 by A3, A9, A10, A15, AFF_1:39, AFF_1:41; hence contradiction by A4, A7, A11, A16, A283, A298, A304, AFF_1:14, AFF_1:25; ::_thesis: verum end; A305: now__::_thesis:_not_c_=_c1 assume c = c1 ; ::_thesis: contradiction then c,a // c,a1 by A21, AFF_1:4; then A306: LIN c,a,a1 by AFF_1:def_1; o,a // o,a1 by A3, A9, A10, A15, AFF_1:39, AFF_1:41; hence contradiction by A5, A8, A13, A17, A283, A298, A306, AFF_1:14, AFF_1:25; ::_thesis: verum end; assume ( not a <> a1 or not b <> b1 or not c <> c1 ) ; ::_thesis: contradiction hence contradiction by A298, A303, A305; ::_thesis: verum end; A307: ( a1 <> o & b1 <> o & c1 <> o ) proof A308: now__::_thesis:_not_a1_=_o assume A309: a1 = o ; ::_thesis: contradiction A310: o = c1 proof A311: not LIN c,a,o proof assume LIN c,a,o ; ::_thesis: contradiction then LIN o,c,a by AFF_1:6; hence contradiction by A5, A8, A13, A17, A283, AFF_1:25; ::_thesis: verum end; assume A312: o <> c1 ; ::_thesis: contradiction A313: o,c1 // o,c by A5, A13, A14, A17, AFF_1:39, AFF_1:41; then a,c // o,c by A21, A309, A312, AFF_1:5; then c,o // c,a by AFF_1:4; then LIN c,o,a by AFF_1:def_1; then LIN o,c,a by AFF_1:6; then o,c // o,a by AFF_1:def_1; then o,c1 // o,a by A8, A313, AFF_1:5; then LIN o,c1,a by AFF_1:def_1; then LIN a,o,c1 by AFF_1:6; then A314: a,o // a,c1 by AFF_1:def_1; c,o // c,c1 by A5, A13, A14, A17, AFF_1:39, AFF_1:41; then LIN c,o,c1 by AFF_1:def_1; hence contradiction by A312, A311, A314, AFF_1:14; ::_thesis: verum end; o = b1 proof A315: not LIN b,a,o proof assume LIN b,a,o ; ::_thesis: contradiction then LIN o,b,a by AFF_1:6; hence contradiction by A4, A7, A11, A16, A283, AFF_1:25; ::_thesis: verum end; assume A316: o <> b1 ; ::_thesis: contradiction A317: o,b1 // o,b by A4, A11, A12, A16, AFF_1:39, AFF_1:41; then a,b // o,b by A20, A309, A316, AFF_1:5; then b,a // b,o by AFF_1:4; then LIN b,a,o by AFF_1:def_1; then LIN o,a,b by AFF_1:6; then o,a // o,b by AFF_1:def_1; then o,a // o,b1 by A7, A317, AFF_1:5; then LIN o,a,b1 by AFF_1:def_1; then LIN a,o,b1 by AFF_1:6; then A318: a,o // a,b1 by AFF_1:def_1; b,o // b,b1 by A4, A11, A12, A16, AFF_1:39, AFF_1:41; then LIN b,o,b1 by AFF_1:def_1; hence contradiction by A316, A315, A318, AFF_1:14; ::_thesis: verum end; hence contradiction by A22, A310, AFF_1:3; ::_thesis: verum end; A319: now__::_thesis:_not_b1_=_o A320: not LIN a,b,o proof assume LIN a,b,o ; ::_thesis: contradiction then LIN o,b,a by AFF_1:6; hence contradiction by A4, A7, A11, A16, A283, AFF_1:25; ::_thesis: verum end; A321: a1,o // a,a1 by A3, A9, A10, A15, AFF_1:39, AFF_1:41; assume b1 = o ; ::_thesis: contradiction then a,b // a,a1 by A20, A308, A321, AFF_1:5; then LIN a,b,a1 by AFF_1:def_1; then LIN a1,b,a by AFF_1:6; then a1,b // a1,a by AFF_1:def_1; then a1,b // a,a1 by AFF_1:4; then a1,b // a1,o by A297, A321, AFF_1:5; then LIN a1,b,o by AFF_1:def_1; then LIN b,o,a1 by AFF_1:6; then A322: b,o // b,a1 by AFF_1:def_1; a,o // a,a1 by A3, A9, A10, A15, AFF_1:39, AFF_1:41; then LIN a,o,a1 by AFF_1:def_1; hence contradiction by A308, A320, A322, AFF_1:14; ::_thesis: verum end; A323: now__::_thesis:_not_c1_=_o A324: not LIN a,c,o proof assume LIN a,c,o ; ::_thesis: contradiction then LIN o,c,a by AFF_1:6; hence contradiction by A5, A8, A13, A17, A283, AFF_1:25; ::_thesis: verum end; A325: a1,o // a,a1 by A3, A9, A10, A15, AFF_1:39, AFF_1:41; assume c1 = o ; ::_thesis: contradiction then a,c // a,a1 by A21, A308, A325, AFF_1:5; then LIN a,c,a1 by AFF_1:def_1; then LIN a1,a,c by AFF_1:6; then a1,a // a1,c by AFF_1:def_1; then a,a1 // a1,c by AFF_1:4; then a1,o // a1,c by A297, A325, AFF_1:5; then LIN a1,o,c by AFF_1:def_1; then LIN c,o,a1 by AFF_1:6; then A326: c,o // c,a1 by AFF_1:def_1; a,o // a,a1 by A3, A9, A10, A15, AFF_1:39, AFF_1:41; then LIN a,o,a1 by AFF_1:def_1; hence contradiction by A308, A324, A326, AFF_1:14; ::_thesis: verum end; assume ( not a1 <> o or not b1 <> o or not c1 <> o ) ; ::_thesis: contradiction hence contradiction by A308, A319, A323; ::_thesis: verum end; ex d2 being Element of X st ( a,c // d,d2 & d2 in M ) proof consider e1 being Element of X such that A327: o,c // o,e1 and A328: o <> e1 by DIRAF:40; consider e2 being Element of X such that A329: a,c // d,e2 and A330: d <> e2 by DIRAF:40; not o,e1 // d,e2 proof assume o,e1 // d,e2 ; ::_thesis: contradiction then o,c // d,e2 by A327, A328, AFF_1:5; then o,c // a,c by A329, A330, AFF_1:5; then c,o // c,a by AFF_1:4; then LIN c,o,a by AFF_1:def_1; hence contradiction by A5, A8, A13, A17, A283, AFF_1:25; ::_thesis: verum end; then consider d2 being Element of X such that A331: LIN o,e1,d2 and A332: LIN d,e2,d2 by AFF_1:60; o,e1 // o,d2 by A331, AFF_1:def_1; then o,c // o,d2 by A327, A328, AFF_1:5; then A333: LIN o,c,d2 by AFF_1:def_1; take d2 ; ::_thesis: ( a,c // d,d2 & d2 in M ) d,e2 // d,d2 by A332, AFF_1:def_1; hence ( a,c // d,d2 & d2 in M ) by A5, A8, A13, A17, A329, A330, A333, AFF_1:5, AFF_1:25; ::_thesis: verum end; then consider d2 being Element of X such that A334: a,c // d,d2 and A335: d2 in M ; consider d1 being Element of X such that A336: a,b // d,d1 and A337: d1 in Z by A288; assume A338: not Z // M ; ::_thesis: contradiction A339: d1 <> d2 proof A340: o <> d1 proof A341: o <> d proof assume o = d ; ::_thesis: contradiction then LIN o,b,c by A280, AFF_1:6; then c in Z by A4, A7, A11, A16, AFF_1:25; then A342: o,c // Z by A4, A16, AFF_1:52; o,c // M by A5, A13, A17, AFF_1:52; hence contradiction by A8, A338, A342, AFF_1:53; ::_thesis: verum end; A343: a,a1 // a,d by A282, AFF_1:def_1; a,o // a,a1 by A3, A9, A10, A15, AFF_1:39, AFF_1:41; then a,o // a,d by A297, A343, AFF_1:5; then LIN a,o,d by AFF_1:def_1; then LIN o,a,d by AFF_1:6; then o,a // o,d by AFF_1:def_1; then A344: a,o // d,o by AFF_1:4; assume o = d1 ; ::_thesis: contradiction then a,b // a,o by A336, A341, A344, AFF_1:5; then LIN a,b,o by AFF_1:def_1; then LIN o,b,a by AFF_1:6; hence contradiction by A4, A7, A11, A16, A283, AFF_1:25; ::_thesis: verum end; assume d1 = d2 ; ::_thesis: contradiction then A345: o,d1 // M by A5, A17, A335, AFF_1:52; o,d1 // Z by A4, A16, A337, AFF_1:52; hence contradiction by A338, A345, A340, AFF_1:53; ::_thesis: verum end; A346: now__::_thesis:_not_b1,c1_//_d1,d2 assume A347: b1,c1 // d1,d2 ; ::_thesis: contradiction ex d5 being Element of X st ( LIN b,c,d5 & LIN d1,d2,d5 ) proof consider e1 being Element of X such that A348: b,c // b,e1 and A349: b <> e1 by DIRAF:40; consider e2 being Element of X such that A350: d1,d2 // d1,e2 and A351: d1 <> e2 by DIRAF:40; not b,e1 // d1,e2 proof assume b,e1 // d1,e2 ; ::_thesis: contradiction then b,e1 // d1,d2 by A350, A351, AFF_1:5; then b,c // d1,d2 by A348, A349, AFF_1:5; hence contradiction by A22, A339, A347, AFF_1:5; ::_thesis: verum end; then consider d5 being Element of X such that A352: LIN b,e1,d5 and A353: LIN d1,e2,d5 by AFF_1:60; b,e1 // b,d5 by A352, AFF_1:def_1; then A354: b,c // b,d5 by A348, A349, AFF_1:5; take d5 ; ::_thesis: ( LIN b,c,d5 & LIN d1,d2,d5 ) d1,e2 // d1,d5 by A353, AFF_1:def_1; then d1,d2 // d1,d5 by A350, A351, AFF_1:5; hence ( LIN b,c,d5 & LIN d1,d2,d5 ) by A354, AFF_1:def_1; ::_thesis: verum end; then consider d5 being Element of X such that A355: LIN b,c,d5 and A356: LIN d1,d2,d5 ; A357: d in Y by A9, A10, A15, A297, A282, AFF_1:25; A358: now__::_thesis:_not_LIN_a,d,d5 A359: not LIN a,b,d proof A360: a <> d proof A361: a1 <> b1 proof o,a1 // o,a by A3, A9, A10, A15, AFF_1:39, AFF_1:41; then A362: LIN o,a1,a by AFF_1:def_1; assume a1 = b1 ; ::_thesis: contradiction hence contradiction by A4, A12, A16, A283, A307, A362, AFF_1:25; ::_thesis: verum end; assume A363: a = d ; ::_thesis: contradiction then LIN a,b,c by A280, AFF_1:6; then a,b // a,c by AFF_1:def_1; then a1,b1 // a,c by A11, A20, A283, AFF_1:5; then a1,b1 // a1,c1 by A13, A21, A283, AFF_1:5; then LIN a1,b1,c1 by AFF_1:def_1; then LIN b1,c1,a1 by AFF_1:6; then b1,c1 // b1,a1 by AFF_1:def_1; then A364: b1,c1 // a1,b1 by AFF_1:4; b,c // b,a by A280, A363, AFF_1:def_1; then b,c // a,b by AFF_1:4; then b,c // a1,b1 by A11, A20, A283, AFF_1:5; hence contradiction by A22, A364, A361, AFF_1:5; ::_thesis: verum end; assume LIN a,b,d ; ::_thesis: contradiction then LIN a,d,b by AFF_1:6; then b in Y by A9, A15, A357, A360, AFF_1:25; then A365: o,b // Y by A3, A15, AFF_1:52; o,b // Z by A4, A11, A16, AFF_1:52; hence contradiction by A3, A4, A7, A18, A365, AFF_1:45, AFF_1:53; ::_thesis: verum end; assume A366: LIN a,d,d5 ; ::_thesis: contradiction A367: o <> d proof A368: o,b // o,b1 by A4, A11, A12, A16, AFF_1:39, AFF_1:41; assume A369: o = d ; ::_thesis: contradiction then LIN o,b,c by A280, AFF_1:6; then o,b // o,c by AFF_1:def_1; then A370: o,b1 // o,c by A7, A368, AFF_1:5; o,c // o,c1 by A5, A13, A14, A17, AFF_1:39, AFF_1:41; then o,b1 // o,c1 by A8, A370, AFF_1:5; then LIN o,b1,c1 by AFF_1:def_1; then LIN b1,c1,o by AFF_1:6; then b1,c1 // b1,o by AFF_1:def_1; then A371: b1,c1 // o,b1 by AFF_1:4; b,c // b,o by A280, A369, AFF_1:def_1; then b,c // o,b by AFF_1:4; then b,c // o,b1 by A7, A368, AFF_1:5; hence contradiction by A22, A307, A371, AFF_1:5; ::_thesis: verum end; A372: d <> d1 proof assume d = d1 ; ::_thesis: contradiction then A373: o,d // Z by A4, A16, A337, AFF_1:52; o,d // Y by A3, A15, A357, AFF_1:52; hence contradiction by A3, A4, A18, A367, A373, AFF_1:45, AFF_1:53; ::_thesis: verum end; A374: d <> d2 proof assume d = d2 ; ::_thesis: contradiction then A375: o,d // M by A5, A17, A335, AFF_1:52; o,d // Y by A3, A15, A357, AFF_1:52; hence contradiction by A3, A5, A19, A367, A375, AFF_1:45, AFF_1:53; ::_thesis: verum end; A376: b,c // b,d5 by A355, AFF_1:def_1; A377: b,c // b,d by A280, AFF_1:def_1; b <> c by A22, AFF_1:3; then b,d // b,d5 by A377, A376, AFF_1:5; then LIN d1,d2,d by A356, A366, A359, AFF_1:14; then LIN d,d1,d2 by AFF_1:6; then d,d1 // d,d2 by AFF_1:def_1; then a,b // d,d2 by A336, A372, AFF_1:5; then A378: a,b // a,c by A334, A374, AFF_1:5; then LIN a,b,c by AFF_1:def_1; then LIN b,c,a by AFF_1:6; then b,c // b,a by AFF_1:def_1; then b,c // a,b by AFF_1:4; then A379: b,c // a1,b1 by A11, A20, A283, AFF_1:5; a1,b1 // a,c by A11, A20, A283, A378, AFF_1:5; then a1,b1 // a1,c1 by A13, A21, A283, AFF_1:5; then LIN a1,b1,c1 by AFF_1:def_1; then LIN b1,c1,a1 by AFF_1:6; then b1,c1 // b1,a1 by AFF_1:def_1; then A380: b1,c1 // a1,b1 by AFF_1:4; a1 <> b1 proof o,a1 // o,a by A3, A9, A10, A15, AFF_1:39, AFF_1:41; then A381: LIN o,a1,a by AFF_1:def_1; assume a1 = b1 ; ::_thesis: contradiction hence contradiction by A4, A12, A16, A283, A307, A381, AFF_1:25; ::_thesis: verum end; hence contradiction by A22, A380, A379, AFF_1:5; ::_thesis: verum end; not b,c // d1,d2 by A22, A339, A347, AFF_1:5; hence contradiction by A2, A3, A4, A5, A6, A7, A8, A9, A11, A13, A15, A16, A17, A18, A19, A23, A336, A337, A334, A335, A355, A356, A357, A358; ::_thesis: verum end; now__::_thesis:_b1,c1_//_d1,d2 A382: d in Y by A9, A10, A15, A297, A282, AFF_1:25; A383: not LIN a1,b1,d proof A384: a1 <> d proof A385: ( a1 <> b1 & a1 <> c1 ) proof o,a1 // o,a by A3, A9, A10, A15, AFF_1:39, AFF_1:41; then A386: LIN o,a1,a by AFF_1:def_1; assume ( not a1 <> b1 or not a1 <> c1 ) ; ::_thesis: contradiction hence contradiction by A4, A5, A12, A14, A16, A17, A283, A307, A386, AFF_1:25; ::_thesis: verum end; assume A387: a1 = d ; ::_thesis: contradiction then LIN a1,b1,c1 by A281, AFF_1:6; then a1,b1 // a1,c1 by AFF_1:def_1; then a,b // a1,c1 by A20, A385, AFF_1:5; then a,b // a,c by A21, A385, AFF_1:5; then LIN a,b,c by AFF_1:def_1; then LIN b,c,a by AFF_1:6; then b,c // b,a by AFF_1:def_1; then A388: b,c // a,b by AFF_1:4; b1,c1 // b1,a1 by A281, A387, AFF_1:def_1; then b1,c1 // a1,b1 by AFF_1:4; then b1,c1 // a,b by A20, A385, AFF_1:5; hence contradiction by A11, A22, A283, A388, AFF_1:5; ::_thesis: verum end; assume LIN a1,b1,d ; ::_thesis: contradiction then LIN a1,d,b1 by AFF_1:6; then b1 in Y by A10, A15, A382, A384, AFF_1:25; then o,b1 // o,a by A3, A9, A15, AFF_1:39, AFF_1:41; then LIN o,b1,a by AFF_1:def_1; hence contradiction by A4, A12, A16, A283, A307, AFF_1:25; ::_thesis: verum end; A389: d <> o proof A390: o,b // o,b1 by A4, A11, A12, A16, AFF_1:39, AFF_1:41; assume A391: d = o ; ::_thesis: contradiction then LIN o,b,c by A280, AFF_1:6; then o,b // o,c by AFF_1:def_1; then A392: o,b1 // o,c by A7, A390, AFF_1:5; o,c // o,c1 by A5, A13, A14, A17, AFF_1:39, AFF_1:41; then o,b1 // o,c1 by A8, A392, AFF_1:5; then LIN o,b1,c1 by AFF_1:def_1; then LIN b1,c1,o by AFF_1:6; then b1,c1 // b1,o by AFF_1:def_1; then A393: b1,c1 // o,b1 by AFF_1:4; b,c // b,o by A280, A391, AFF_1:def_1; then b,c // o,b by AFF_1:4; then b,c // o,b1 by A7, A390, AFF_1:5; hence contradiction by A22, A307, A393, AFF_1:5; ::_thesis: verum end; A394: d <> d1 proof o,d // o,a by A3, A9, A15, A382, AFF_1:39, AFF_1:41; then A395: LIN o,d,a by AFF_1:def_1; assume d = d1 ; ::_thesis: contradiction hence contradiction by A4, A16, A283, A337, A389, A395, AFF_1:25; ::_thesis: verum end; A396: d <> d2 proof o,d // o,a by A3, A9, A15, A382, AFF_1:39, AFF_1:41; then A397: LIN o,d,a by AFF_1:def_1; assume d = d2 ; ::_thesis: contradiction hence contradiction by A5, A17, A283, A335, A389, A397, AFF_1:25; ::_thesis: verum end; A398: a1,c1 // d,d2 by A13, A21, A283, A334, AFF_1:5; A399: b1 <> c1 by A22, AFF_1:3; A400: b1,c1 // b1,d by A281, AFF_1:def_1; assume A401: not b1,c1 // d1,d2 ; ::_thesis: contradiction then consider d5 being Element of X such that A402: LIN b1,c1,d5 and A403: LIN d1,d2,d5 by AFF_1:60; b1,c1 // b1,d5 by A402, AFF_1:def_1; then A404: b1,d // b1,d5 by A399, A400, AFF_1:5; a1,b1 // d,d1 by A11, A20, A283, A336, AFF_1:5; then LIN a1,d,d5 by A2, A3, A4, A5, A10, A12, A14, A15, A16, A17, A18, A19, A23, A307, A337, A335, A401, A402, A403, A382, A398; then d = d5 by A383, A404, AFF_1:14; then LIN d,d1,d2 by A403, AFF_1:6; then d,d1 // d,d2 by AFF_1:def_1; then a,b // d,d2 by A336, A394, AFF_1:5; then A405: a,b // a,c by A334, A396, AFF_1:5; then LIN a,b,c by AFF_1:def_1; then LIN b,c,a by AFF_1:6; then b,c // b,a by AFF_1:def_1; then b,c // a,b by AFF_1:4; then A406: b,c // a1,b1 by A11, A20, A283, AFF_1:5; a1,b1 // a,c by A11, A20, A283, A405, AFF_1:5; then a1,b1 // a1,c1 by A13, A21, A283, AFF_1:5; then LIN a1,b1,c1 by AFF_1:def_1; then LIN b1,c1,a1 by AFF_1:6; then b1,c1 // b1,a1 by AFF_1:def_1; then A407: b1,c1 // a1,b1 by AFF_1:4; a1 <> b1 proof o,a1 // o,a by A3, A9, A10, A15, AFF_1:39, AFF_1:41; then A408: LIN o,a1,a by AFF_1:def_1; assume a1 = b1 ; ::_thesis: contradiction hence contradiction by A4, A12, A16, A283, A307, A408, AFF_1:25; ::_thesis: verum end; hence contradiction by A22, A407, A406, AFF_1:5; ::_thesis: verum end; hence contradiction by A346; ::_thesis: verum end; now__::_thesis:_not_Z_//_M assume A409: Z // M ; ::_thesis: contradiction then A410: b1 in M by A4, A5, A12, AFF_1:45; b in M by A4, A5, A11, A409, AFF_1:45; hence contradiction by A13, A14, A17, A22, A410, AFF_1:39, AFF_1:41; ::_thesis: verum end; hence contradiction by A278; ::_thesis: verum end; hence X is Desarguesian by AFF_2:def_4; ::_thesis: verum end; ( X is Desarguesian implies X is satisfying_Scherungssatz ) proof assume A411: X is Desarguesian ; ::_thesis: X is satisfying_Scherungssatz then X is satisfying_TDES_1 by AFF_2:3, AFF_2:12; then X is satisfying_des_1 by AFF_2:13; then X is translational by AFF_2:7; then A412: X is satisfying_minor_Scherungssatz by Th6; X is satisfying_major_Scherungssatz by A411, Th7; hence X is satisfying_Scherungssatz by A412, Th2; ::_thesis: verum end; hence ( X is Desarguesian iff X is satisfying_Scherungssatz ) by A1; ::_thesis: verum end; theorem Th9: :: CONMETR1:9 for X being AffinPlane holds ( X is satisfying_pap iff X is satisfying_minor_indirect_Scherungssatz ) proof let X be AffinPlane; ::_thesis: ( X is satisfying_pap iff X is satisfying_minor_indirect_Scherungssatz ) A1: ( X is satisfying_minor_indirect_Scherungssatz implies X is satisfying_pap ) proof assume A2: X is satisfying_minor_indirect_Scherungssatz ; ::_thesis: X is satisfying_pap now__::_thesis:_for_M,_N_being_Subset_of_X for_a,_b,_c,_a1,_b1,_c1_being_Element_of_X_st_M_is_being_line_&_N_is_being_line_&_a_in_M_&_b_in_M_&_c_in_M_&_M_//_N_&_M_<>_N_&_a1_in_N_&_b1_in_N_&_c1_in_N_&_a,b1_//_b,a1_&_b,c1_//_c,b1_holds_ a,c1_//_c,a1 let M, N be Subset of X; ::_thesis: for a, b, c, a1, b1, c1 being Element of X st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 holds a,c1 // c,a1 let a, b, c, a1, b1, c1 be Element of X; ::_thesis: ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 implies a,c1 // c,a1 ) assume that M is being_line and N is being_line and A3: a in M and A4: b in M and A5: c in M and A6: M // N and A7: M <> N and A8: a1 in N and A9: b1 in N and A10: c1 in N and A11: a,b1 // b,a1 and A12: b,c1 // c,b1 ; ::_thesis: a,c1 // c,a1 A13: not b in N by A4, A6, A7, AFF_1:45; A14: not c1 in M by A6, A7, A10, AFF_1:45; A15: not c in N by A5, A6, A7, AFF_1:45; A16: b1,b // b,b1 by AFF_1:2; A17: not b1 in M by A6, A7, A9, AFF_1:45; A18: b,c1 // b1,c by A12, AFF_1:4; A19: not a1 in M by A6, A7, A8, AFF_1:45; A20: a,b1 // a1,b by A11, AFF_1:4; not a in N by A3, A6, A7, AFF_1:45; then a,c1 // a1,c by A2, A3, A4, A5, A6, A8, A9, A10, A13, A15, A19, A17, A14, A20, A18, A16, Def5; hence a,c1 // c,a1 by AFF_1:4; ::_thesis: verum end; hence X is satisfying_pap by AFF_2:def_13; ::_thesis: verum end; ( X is satisfying_pap implies X is satisfying_minor_indirect_Scherungssatz ) proof assume A21: X is satisfying_pap ; ::_thesis: X is satisfying_minor_indirect_Scherungssatz now__::_thesis:_for_a1,_a2,_a3,_a4,_b1,_b2,_b3,_b4_being_Element_of_X for_M,_N_being_Subset_of_X_st_M_//_N_&_a1_in_M_&_a3_in_M_&_b2_in_M_&_b4_in_M_&_a2_in_N_&_a4_in_N_&_b1_in_N_&_b3_in_N_&_not_a4_in_M_&_not_a2_in_M_&_not_b1_in_M_&_not_b3_in_M_&_not_a1_in_N_&_not_a3_in_N_&_not_b2_in_N_&_not_b4_in_N_&_a3,a2_//_b3,b2_&_a2,a1_//_b2,b1_&_a1,a4_//_b1,b4_holds_ a3,a4_//_b3,b4 let a1, a2, a3, a4, b1, b2, b3, b4 be Element of X; ::_thesis: for M, N being Subset of X st M // N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 let M, N be Subset of X; ::_thesis: ( M // N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 ) assume that A22: M // N and A23: a1 in M and A24: a3 in M and A25: b2 in M and A26: b4 in M and A27: a2 in N and A28: a4 in N and A29: b1 in N and A30: b3 in N and A31: not a4 in M and not a2 in M and not b1 in M and not b3 in M and not a1 in N and not a3 in N and not b2 in N and not b4 in N and A32: a3,a2 // b3,b2 and A33: a2,a1 // b2,b1 and A34: a1,a4 // b1,b4 ; ::_thesis: a3,a4 // b3,b4 A35: M is being_line by A22, AFF_1:36; A36: b2,b3 // a3,a2 by A32, AFF_1:4; A37: N is being_line by A22, AFF_1:36; A38: a4,a1 // b1,b4 by A34, AFF_1:4; a1,a2 // b2,b1 by A33, AFF_1:4; then a1,b3 // a3,b1 by A21, A22, A23, A24, A25, A27, A28, A29, A30, A31, A35, A37, A36, AFF_2:def_13; then b1,a3 // b3,a1 by AFF_1:4; then a4,a3 // b3,b4 by A21, A22, A23, A24, A26, A28, A29, A30, A31, A35, A37, A38, AFF_2:def_13; hence a3,a4 // b3,b4 by AFF_1:4; ::_thesis: verum end; hence X is satisfying_minor_indirect_Scherungssatz by Def5; ::_thesis: verum end; hence ( X is satisfying_pap iff X is satisfying_minor_indirect_Scherungssatz ) by A1; ::_thesis: verum end; theorem Th10: :: CONMETR1:10 for X being AffinPlane holds ( X is Pappian iff X is satisfying_major_indirect_Scherungssatz ) proof let X be AffinPlane; ::_thesis: ( X is Pappian iff X is satisfying_major_indirect_Scherungssatz ) A1: ( X is Pappian implies X is satisfying_major_indirect_Scherungssatz ) proof assume A2: X is Pappian ; ::_thesis: X is satisfying_major_indirect_Scherungssatz then A3: X is Desarguesian by AFF_2:11; now__::_thesis:_for_o,_a1,_a2,_a3,_a4,_b1,_b2,_b3,_b4_being_Element_of_X for_M,_N_being_Subset_of_X_st_M_is_being_line_&_N_is_being_line_&_o_in_M_&_o_in_N_&_a1_in_M_&_a3_in_M_&_b2_in_M_&_b4_in_M_&_a2_in_N_&_a4_in_N_&_b1_in_N_&_b3_in_N_&_not_a4_in_M_&_not_a2_in_M_&_not_b1_in_M_&_not_b3_in_M_&_not_a1_in_N_&_not_a3_in_N_&_not_b2_in_N_&_not_b4_in_N_&_a3,a2_//_b3,b2_&_a2,a1_//_b2,b1_&_a1,a4_//_b1,b4_holds_ a3,a4_//_b3,b4 let o, a1, a2, a3, a4, b1, b2, b3, b4 be Element of X; ::_thesis: for M, N being Subset of X st M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 let M, N be Subset of X; ::_thesis: ( M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 ) assume that A4: M is being_line and A5: N is being_line and A6: o in M and A7: o in N and A8: a1 in M and A9: a3 in M and A10: b2 in M and A11: b4 in M and A12: a2 in N and A13: a4 in N and A14: b1 in N and A15: b3 in N and A16: not a4 in M and A17: not a2 in M and A18: not b1 in M and A19: not b3 in M and A20: not a1 in N and A21: not a3 in N and A22: not b2 in N and A23: not b4 in N and A24: a3,a2 // b3,b2 and A25: a2,a1 // b2,b1 and A26: a1,a4 // b1,b4 ; ::_thesis: a3,a4 // b3,b4 A27: now__::_thesis:_(_a1_<>_a3_&_a2_<>_a4_implies_a3,a4_//_b3,b4_) assume that A28: a1 <> a3 and A29: a2 <> a4 ; ::_thesis: a3,a4 // b3,b4 ex x, y, z being Element of X st ( LIN x,y,z & x <> y & x <> z & y <> z ) proof o,a1 // o,a3 by A4, A6, A8, A9, AFF_1:39, AFF_1:41; then A30: LIN o,a1,a3 by AFF_1:def_1; assume for x, y, z being Element of X holds ( not LIN x,y,z or not x <> y or not x <> z or not y <> z ) ; ::_thesis: contradiction hence contradiction by A7, A20, A21, A28, A30; ::_thesis: verum end; then consider d being Element of X such that A31: LIN a2,a1,d and A32: a2 <> d and A33: a1 <> d by TRANSLAC:1; A34: a2,a1 // a2,d by A31, AFF_1:def_1; A35: ex c2 being Element of X st ( c2 in M & a2,a3 // b1,c2 ) proof consider e2 being Element of X such that A36: a1,a3 // a1,e2 and A37: a1 <> e2 by DIRAF:40; consider e1 being Element of X such that A38: a2,a3 // b1,e1 and A39: b1 <> e1 by DIRAF:40; not b1,e1 // a1,e2 proof assume b1,e1 // a1,e2 ; ::_thesis: contradiction then a2,a3 // a1,e2 by A38, A39, AFF_1:5; then a2,a3 // a1,a3 by A36, A37, AFF_1:5; then a3,a1 // a3,a2 by AFF_1:4; then LIN a3,a1,a2 by AFF_1:def_1; hence contradiction by A4, A8, A9, A17, A28, AFF_1:25; ::_thesis: verum end; then consider c2 being Element of X such that A40: LIN b1,e1,c2 and A41: LIN a1,e2,c2 by AFF_1:60; a1,e2 // a1,c2 by A41, AFF_1:def_1; then a1,a3 // a1,c2 by A36, A37, AFF_1:5; then A42: LIN a1,a3,c2 by AFF_1:def_1; take c2 ; ::_thesis: ( c2 in M & a2,a3 // b1,c2 ) b1,e1 // b1,c2 by A40, AFF_1:def_1; hence ( c2 in M & a2,a3 // b1,c2 ) by A4, A8, A9, A28, A38, A39, A42, AFF_1:5, AFF_1:25; ::_thesis: verum end; A43: ex c1 being Element of X st ( c1 in N & a1,a4 // b2,c1 ) proof consider e2 being Element of X such that A44: a2,a4 // a2,e2 and A45: a2 <> e2 by DIRAF:40; consider e1 being Element of X such that A46: a1,a4 // b2,e1 and A47: b2 <> e1 by DIRAF:40; not b2,e1 // a2,e2 proof assume b2,e1 // a2,e2 ; ::_thesis: contradiction then a1,a4 // a2,e2 by A46, A47, AFF_1:5; then a1,a4 // a2,a4 by A44, A45, AFF_1:5; then a4,a2 // a4,a1 by AFF_1:4; then LIN a4,a2,a1 by AFF_1:def_1; hence contradiction by A5, A12, A13, A20, A29, AFF_1:25; ::_thesis: verum end; then consider c1 being Element of X such that A48: LIN b2,e1,c1 and A49: LIN a2,e2,c1 by AFF_1:60; a2,e2 // a2,c1 by A49, AFF_1:def_1; then a2,a4 // a2,c1 by A44, A45, AFF_1:5; then A50: LIN a2,a4,c1 by AFF_1:def_1; take c1 ; ::_thesis: ( c1 in N & a1,a4 // b2,c1 ) b2,e1 // b2,c1 by A48, AFF_1:def_1; hence ( c1 in N & a1,a4 // b2,c1 ) by A5, A12, A13, A29, A46, A47, A50, AFF_1:5, AFF_1:25; ::_thesis: verum end; consider c2 being Element of X such that A51: c2 in M and A52: a2,a3 // b1,c2 by A35; consider c1 being Element of X such that A53: c1 in N and A54: a1,a4 // b2,c1 by A43; b1,b4 // b2,c1 by A8, A16, A26, A54, AFF_1:5; then A55: b4,b1 // b2,c1 by AFF_1:4; A56: ( o <> c1 & o <> c2 ) proof A57: now__::_thesis:_not_o_=_c2 assume o = c2 ; ::_thesis: contradiction then A58: o,b1 // a2,a3 by A52, AFF_1:4; o,b1 // a2,a4 by A5, A7, A12, A13, A14, AFF_1:39, AFF_1:41; then a2,a4 // a2,a3 by A6, A18, A58, AFF_1:5; then LIN a2,a4,a3 by AFF_1:def_1; hence contradiction by A5, A12, A13, A21, A29, AFF_1:25; ::_thesis: verum end; A59: now__::_thesis:_not_o_=_c1 assume o = c1 ; ::_thesis: contradiction then A60: o,b2 // a1,a4 by A54, AFF_1:4; o,b2 // a1,a3 by A4, A6, A8, A9, A10, AFF_1:39, AFF_1:41; then a1,a3 // a1,a4 by A7, A22, A60, AFF_1:5; then LIN a1,a3,a4 by AFF_1:def_1; hence contradiction by A4, A8, A9, A16, A28, AFF_1:25; ::_thesis: verum end; assume ( not o <> c1 or not o <> c2 ) ; ::_thesis: contradiction hence contradiction by A59, A57; ::_thesis: verum end; a3,a2 // c2,b1 by A52, AFF_1:4; then b3,b2 // c2,b1 by A9, A17, A24, AFF_1:5; then b2,b3 // c2,b1 by AFF_1:4; then A61: b4,b3 // c2,c1 by A2, A4, A5, A6, A7, A10, A11, A14, A15, A18, A19, A22, A23, A53, A51, A56, A55, AFF_2:def_2; LIN a1,a2,d by A31, AFF_1:6; then a1,a2 // a1,d by AFF_1:def_1; then a2,a1 // a1,d by AFF_1:4; then A62: b2,b1 // a1,d by A8, A17, A25, AFF_1:5; A63: b1 <> b3 proof assume b1 = b3 ; ::_thesis: contradiction then b2,b1 // a2,a3 by A24, AFF_1:4; then A64: a2,a1 // a2,a3 by A10, A18, A25, AFF_1:5; o,a1 // o,a3 by A4, A6, A8, A9, AFF_1:39, AFF_1:41; then LIN o,a1,a3 by AFF_1:def_1; hence contradiction by A5, A6, A7, A12, A17, A20, A28, A64, AFF_1:14, AFF_1:25; ::_thesis: verum end; A65: c1 <> c2 proof A66: b1 <> c1 proof assume b1 = c1 ; ::_thesis: contradiction then a1,a4 // a2,a1 by A10, A18, A25, A54, AFF_1:5; then a1,a4 // a1,a2 by AFF_1:4; then LIN a1,a4,a2 by AFF_1:def_1; then LIN a2,a4,a1 by AFF_1:6; hence contradiction by A5, A12, A13, A20, A29, AFF_1:25; ::_thesis: verum end; assume c1 = c2 ; ::_thesis: contradiction then a3,a2 // b1,c1 by A52, AFF_1:4; then A67: b3,b2 // b1,c1 by A9, A17, A24, AFF_1:5; b1,c1 // b3,b1 by A5, A14, A15, A53, AFF_1:39, AFF_1:41; then b3,b1 // b3,b2 by A67, A66, AFF_1:5; then LIN b3,b1,b2 by AFF_1:def_1; hence contradiction by A5, A14, A15, A22, A63, AFF_1:25; ::_thesis: verum end; LIN o,d,d by AFF_1:7; then consider Y being Subset of X such that A68: Y is being_line and A69: o in Y and A70: d in Y and d in Y by AFF_1:21; A71: ( M <> N & M <> Y & N <> Y ) proof A72: now__::_thesis:_not_N_=_Y assume A73: N = Y ; ::_thesis: contradiction LIN a2,d,a1 by A31, AFF_1:6; hence contradiction by A5, A12, A20, A32, A70, A73, AFF_1:25; ::_thesis: verum end; A74: now__::_thesis:_not_M_=_Y assume A75: M = Y ; ::_thesis: contradiction LIN a1,d,a2 by A31, AFF_1:6; hence contradiction by A4, A8, A17, A33, A70, A75, AFF_1:25; ::_thesis: verum end; assume ( not M <> N or not M <> Y or not N <> Y ) ; ::_thesis: contradiction hence contradiction by A13, A16, A74, A72; ::_thesis: verum end; A76: o <> d proof assume o = d ; ::_thesis: contradiction then LIN o,a1,a2 by A31, AFF_1:6; hence contradiction by A4, A6, A7, A8, A17, A20, AFF_1:25; ::_thesis: verum end; ex d1 being Element of X st ( LIN b1,b2,d1 & d1 in Y ) proof consider e2 being Element of X such that A77: o,d // o,e2 and A78: o <> e2 by DIRAF:40; consider e1 being Element of X such that A79: b1,b2 // b1,e1 and A80: b1 <> e1 by DIRAF:40; not b1,e1 // o,e2 proof assume b1,e1 // o,e2 ; ::_thesis: contradiction then b1,b2 // o,e2 by A79, A80, AFF_1:5; then b1,b2 // o,d by A77, A78, AFF_1:5; then b2,b1 // o,d by AFF_1:4; then A81: a2,a1 // o,d by A10, A18, A25, AFF_1:5; a2,a1 // a2,d by A31, AFF_1:def_1; then a2,d // o,d by A8, A17, A81, AFF_1:5; then d,o // d,a2 by AFF_1:4; then LIN d,o,a2 by AFF_1:def_1; then A82: LIN o,a2,d by AFF_1:6; LIN a1,a2,d by A31, AFF_1:6; then a1,a2 // a1,d by AFF_1:def_1; hence contradiction by A4, A6, A7, A8, A17, A20, A32, A82, AFF_1:14, AFF_1:25; ::_thesis: verum end; then consider d1 being Element of X such that A83: LIN b1,e1,d1 and A84: LIN o,e2,d1 by AFF_1:60; o,e2 // o,d1 by A84, AFF_1:def_1; then o,d // o,d1 by A77, A78, AFF_1:5; then A85: LIN o,d,d1 by AFF_1:def_1; take d1 ; ::_thesis: ( LIN b1,b2,d1 & d1 in Y ) b1,e1 // b1,d1 by A83, AFF_1:def_1; then b1,b2 // b1,d1 by A79, A80, AFF_1:5; hence ( LIN b1,b2,d1 & d1 in Y ) by A76, A68, A69, A70, A85, AFF_1:25, AFF_1:def_1; ::_thesis: verum end; then consider d1 being Element of X such that A86: LIN b1,b2,d1 and A87: d1 in Y ; LIN b2,b1,d1 by A86, AFF_1:6; then b2,b1 // b2,d1 by AFF_1:def_1; then a1,d // b2,d1 by A10, A18, A62, AFF_1:5; then A88: d,a4 // d1,c1 by A3, A4, A5, A6, A7, A8, A10, A13, A16, A20, A76, A68, A69, A70, A87, A53, A54, A71, AFF_2:def_4; b1,b2 // b1,d1 by A86, AFF_1:def_1; then b2,b1 // b1,d1 by AFF_1:4; then a2,a1 // b1,d1 by A10, A18, A25, AFF_1:5; then a2,d // b1,d1 by A8, A17, A34, AFF_1:5; then d,a3 // d1,c2 by A3, A4, A5, A6, A7, A9, A12, A14, A17, A21, A76, A68, A69, A70, A87, A51, A52, A71, AFF_2:def_4; then a3,a4 // c2,c1 by A3, A4, A5, A6, A7, A9, A13, A16, A21, A76, A68, A69, A70, A87, A53, A51, A71, A88, AFF_2:def_4; then b4,b3 // a3,a4 by A65, A61, AFF_1:5; hence a3,a4 // b3,b4 by AFF_1:4; ::_thesis: verum end; now__::_thesis:_(_(_a1_=_a3_or_a2_=_a4_)_implies_a3,a4_//_b3,b4_) A89: now__::_thesis:_(_a2_=_a4_implies_a3,a4_//_b3,b4_) o,b2 // o,b4 by A4, A6, A10, A11, AFF_1:39, AFF_1:41; then A90: LIN o,b2,b4 by AFF_1:def_1; assume A91: a2 = a4 ; ::_thesis: a3,a4 // b3,b4 then a1,a4 // b1,b2 by A25, AFF_1:4; then b1,b2 // b1,b4 by A8, A16, A26, AFF_1:5; hence a3,a4 // b3,b4 by A5, A6, A7, A14, A18, A22, A24, A91, A90, AFF_1:14, AFF_1:25; ::_thesis: verum end; A92: now__::_thesis:_(_a1_=_a3_implies_a3,a4_//_b3,b4_) o,b1 // o,b3 by A5, A7, A14, A15, AFF_1:39, AFF_1:41; then A93: LIN o,b1,b3 by AFF_1:def_1; assume A94: a1 = a3 ; ::_thesis: a3,a4 // b3,b4 then a2,a1 // b2,b3 by A24, AFF_1:4; then b2,b1 // b2,b3 by A8, A17, A25, AFF_1:5; hence a3,a4 // b3,b4 by A4, A6, A7, A10, A18, A22, A26, A94, A93, AFF_1:14, AFF_1:25; ::_thesis: verum end; assume ( a1 = a3 or a2 = a4 ) ; ::_thesis: a3,a4 // b3,b4 hence a3,a4 // b3,b4 by A92, A89; ::_thesis: verum end; hence a3,a4 // b3,b4 by A27; ::_thesis: verum end; hence X is satisfying_major_indirect_Scherungssatz by Def6; ::_thesis: verum end; ( X is satisfying_major_indirect_Scherungssatz implies X is Pappian ) proof assume A95: X is satisfying_major_indirect_Scherungssatz ; ::_thesis: X is Pappian now__::_thesis:_for_M,_N_being_Subset_of_X for_o,_a,_b,_c,_a1,_b1,_c1_being_Element_of_X_st_M_is_being_line_&_N_is_being_line_&_M_<>_N_&_o_in_M_&_o_in_N_&_o_<>_a_&_o_<>_a1_&_o_<>_b_&_o_<>_b1_&_o_<>_c_&_o_<>_c1_&_a_in_M_&_b_in_M_&_c_in_M_&_a1_in_N_&_b1_in_N_&_c1_in_N_&_a,b1_//_b,a1_&_b,c1_//_c,b1_holds_ a,c1_//_c,a1 let M, N be Subset of X; ::_thesis: for o, a, b, c, a1, b1, c1 being Element of X st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a in M & b in M & c in M & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 holds a,c1 // c,a1 let o, a, b, c, a1, b1, c1 be Element of X; ::_thesis: ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a in M & b in M & c in M & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 implies a,c1 // c,a1 ) assume that A96: M is being_line and A97: N is being_line and A98: M <> N and A99: o in M and A100: o in N and A101: o <> a and A102: o <> a1 and A103: o <> b and A104: o <> b1 and A105: o <> c and A106: o <> c1 and A107: a in M and A108: b in M and A109: c in M and A110: a1 in N and A111: b1 in N and A112: c1 in N and A113: a,b1 // b,a1 and A114: b,c1 // c,b1 ; ::_thesis: a,c1 // c,a1 A115: ( not a in N & not b in N & not c in N & not a1 in M & not b1 in M & not c1 in M ) proof A116: o,c1 // o,c1 by AFF_1:2; A117: o,b1 // o,b1 by AFF_1:2; A118: o,a1 // o,a1 by AFF_1:2; A119: o,c // o,c by AFF_1:2; A120: o,b // o,b by AFF_1:2; A121: o,a // o,a by AFF_1:2; assume ( a in N or b in N or c in N or a1 in M or b1 in M or c1 in M ) ; ::_thesis: contradiction then M // N by A96, A97, A99, A100, A101, A102, A103, A104, A105, A106, A107, A108, A109, A110, A111, A112, A121, A120, A119, A118, A117, A116, AFF_1:38; hence contradiction by A98, A99, A100, AFF_1:45; ::_thesis: verum end; A122: b,c1 // b1,c by A114, AFF_1:4; A123: b1,b // b,b1 by AFF_1:2; a,b1 // a1,b by A113, AFF_1:4; then a,c1 // a1,c by A95, A96, A97, A99, A100, A107, A108, A109, A110, A111, A112, A115, A122, A123, Def6; hence a,c1 // c,a1 by AFF_1:4; ::_thesis: verum end; hence X is Pappian by AFF_2:def_2; ::_thesis: verum end; hence ( X is Pappian iff X is satisfying_major_indirect_Scherungssatz ) by A1; ::_thesis: verum end; theorem :: CONMETR1:11 for X being AffinPlane holds ( X is satisfying_PPAP iff X is satisfying_indirect_Scherungssatz ) proof let X be AffinPlane; ::_thesis: ( X is satisfying_PPAP iff X is satisfying_indirect_Scherungssatz ) A1: ( X is satisfying_PPAP implies X is satisfying_indirect_Scherungssatz ) proof assume A2: X is satisfying_PPAP ; ::_thesis: X is satisfying_indirect_Scherungssatz then X is satisfying_pap by AFF_2:10; then A3: X is satisfying_minor_indirect_Scherungssatz by Th9; X is Pappian by A2, AFF_2:10; then X is satisfying_major_indirect_Scherungssatz by Th10; hence X is satisfying_indirect_Scherungssatz by A3, Th1; ::_thesis: verum end; ( X is satisfying_indirect_Scherungssatz implies X is satisfying_PPAP ) proof assume A4: X is satisfying_indirect_Scherungssatz ; ::_thesis: X is satisfying_PPAP then X is satisfying_major_indirect_Scherungssatz by Th1; then A5: X is Pappian by Th10; X is satisfying_minor_indirect_Scherungssatz by A4, Th1; then X is satisfying_pap by Th9; hence X is satisfying_PPAP by A5, AFF_2:10; ::_thesis: verum end; hence ( X is satisfying_PPAP iff X is satisfying_indirect_Scherungssatz ) by A1; ::_thesis: verum end; theorem :: CONMETR1:12 for X being AffinPlane st X is satisfying_major_indirect_Scherungssatz holds X is satisfying_minor_indirect_Scherungssatz proof let X be AffinPlane; ::_thesis: ( X is satisfying_major_indirect_Scherungssatz implies X is satisfying_minor_indirect_Scherungssatz ) assume X is satisfying_major_indirect_Scherungssatz ; ::_thesis: X is satisfying_minor_indirect_Scherungssatz then X is Pappian by Th10; then X is satisfying_pap by AFF_2:9; hence X is satisfying_minor_indirect_Scherungssatz by Th9; ::_thesis: verum end; theorem :: CONMETR1:13 for X being OrtAfPl holds ( Af X is satisfying_Scherungssatz iff X is satisfying_SCH ) proof let X be OrtAfPl; ::_thesis: ( Af X is satisfying_Scherungssatz iff X is satisfying_SCH ) A1: ( X is satisfying_SCH implies Af X is satisfying_Scherungssatz ) proof assume A2: X is satisfying_SCH ; ::_thesis: Af X is satisfying_Scherungssatz now__::_thesis:_for_a1,_a2,_a3,_a4,_b1,_b2,_b3,_b4_being_Element_of_(Af_X) for_M,_N_being_Subset_of_(Af_X)_st_M_is_being_line_&_N_is_being_line_&_a1_in_M_&_a3_in_M_&_b1_in_M_&_b3_in_M_&_a2_in_N_&_a4_in_N_&_b2_in_N_&_b4_in_N_&_not_a4_in_M_&_not_a2_in_M_&_not_b2_in_M_&_not_b4_in_M_&_not_a1_in_N_&_not_a3_in_N_&_not_b1_in_N_&_not_b3_in_N_&_a3,a2_//_b3,b2_&_a2,a1_//_b2,b1_&_a1,a4_//_b1,b4_holds_ a3,a4_//_b3,b4 let a1, a2, a3, a4, b1, b2, b3, b4 be Element of (Af X); ::_thesis: for M, N being Subset of (Af X) st M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4 let M, N be Subset of (Af X); ::_thesis: ( M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 ) assume that A3: M is being_line and A4: N is being_line and A5: a1 in M and A6: a3 in M and A7: b1 in M and A8: b3 in M and A9: a2 in N and A10: a4 in N and A11: b2 in N and A12: b4 in N and A13: not a4 in M and A14: not a2 in M and A15: not b2 in M and A16: not b4 in M and A17: not a1 in N and A18: not a3 in N and A19: not b1 in N and A20: not b3 in N and A21: a3,a2 // b3,b2 and A22: a2,a1 // b2,b1 and A23: a1,a4 // b1,b4 ; ::_thesis: a3,a4 // b3,b4 reconsider a19 = a1, a29 = a2, a39 = a3, a49 = a4, b19 = b1, b29 = b2, b39 = b3, b49 = b4 as Element of X by ANALMETR:35; A24: a39,a29 // b39,b29 by A21, ANALMETR:36; A25: a19,a49 // b19,b49 by A23, ANALMETR:36; A26: a29,a19 // b29,b19 by A22, ANALMETR:36; reconsider M9 = M, N9 = N as Subset of X by ANALMETR:42; A27: N9 is being_line by A4, ANALMETR:43; M9 is being_line by A3, ANALMETR:43; then a39,a49 // b39,b49 by A2, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A27, A24, A26, A25, CONMETR:def_6; hence a3,a4 // b3,b4 by ANALMETR:36; ::_thesis: verum end; hence Af X is satisfying_Scherungssatz by Def3; ::_thesis: verum end; ( Af X is satisfying_Scherungssatz implies X is satisfying_SCH ) proof assume A28: Af X is satisfying_Scherungssatz ; ::_thesis: X is satisfying_SCH now__::_thesis:_for_a19,_a29,_a39,_a49,_b19,_b29,_b39,_b49_being_Element_of_X for_M9,_N9_being_Subset_of_X_st_M9_is_being_line_&_N9_is_being_line_&_a19_in_M9_&_a39_in_M9_&_b19_in_M9_&_b39_in_M9_&_a29_in_N9_&_a49_in_N9_&_b29_in_N9_&_b49_in_N9_&_not_a49_in_M9_&_not_a29_in_M9_&_not_b29_in_M9_&_not_b49_in_M9_&_not_a19_in_N9_&_not_a39_in_N9_&_not_b19_in_N9_&_not_b39_in_N9_&_a39,a29_//_b39,b29_&_a29,a19_//_b29,b19_&_a19,a49_//_b19,b49_holds_ a39,a49_//_b39,b49 let a19, a29, a39, a49, b19, b29, b39, b49 be Element of X; ::_thesis: for M9, N9 being Subset of X st M9 is being_line & N9 is being_line & a19 in M9 & a39 in M9 & b19 in M9 & b39 in M9 & a29 in N9 & a49 in N9 & b29 in N9 & b49 in N9 & not a49 in M9 & not a29 in M9 & not b29 in M9 & not b49 in M9 & not a19 in N9 & not a39 in N9 & not b19 in N9 & not b39 in N9 & a39,a29 // b39,b29 & a29,a19 // b29,b19 & a19,a49 // b19,b49 holds a39,a49 // b39,b49 let M9, N9 be Subset of X; ::_thesis: ( M9 is being_line & N9 is being_line & a19 in M9 & a39 in M9 & b19 in M9 & b39 in M9 & a29 in N9 & a49 in N9 & b29 in N9 & b49 in N9 & not a49 in M9 & not a29 in M9 & not b29 in M9 & not b49 in M9 & not a19 in N9 & not a39 in N9 & not b19 in N9 & not b39 in N9 & a39,a29 // b39,b29 & a29,a19 // b29,b19 & a19,a49 // b19,b49 implies a39,a49 // b39,b49 ) assume that A29: M9 is being_line and A30: N9 is being_line and A31: a19 in M9 and A32: a39 in M9 and A33: b19 in M9 and A34: b39 in M9 and A35: a29 in N9 and A36: a49 in N9 and A37: b29 in N9 and A38: b49 in N9 and A39: not a49 in M9 and A40: not a29 in M9 and A41: not b29 in M9 and A42: not b49 in M9 and A43: not a19 in N9 and A44: not a39 in N9 and A45: not b19 in N9 and A46: not b39 in N9 and A47: a39,a29 // b39,b29 and A48: a29,a19 // b29,b19 and A49: a19,a49 // b19,b49 ; ::_thesis: a39,a49 // b39,b49 reconsider a1 = a19, a2 = a29, a3 = a39, a4 = a49, b1 = b19, b2 = b29, b3 = b39, b4 = b49 as Element of (Af X) by ANALMETR:35; A50: a3,a2 // b3,b2 by A47, ANALMETR:36; A51: a1,a4 // b1,b4 by A49, ANALMETR:36; A52: a2,a1 // b2,b1 by A48, ANALMETR:36; reconsider M = M9, N = N9 as Subset of (Af X) by ANALMETR:42; A53: N is being_line by A30, ANALMETR:43; M is being_line by A29, ANALMETR:43; then a3,a4 // b3,b4 by A28, A31, A32, A33, A34, A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A45, A46, A53, A50, A52, A51, Def3; hence a39,a49 // b39,b49 by ANALMETR:36; ::_thesis: verum end; hence X is satisfying_SCH by CONMETR:def_6; ::_thesis: verum end; hence ( Af X is satisfying_Scherungssatz iff X is satisfying_SCH ) by A1; ::_thesis: verum end; theorem :: CONMETR1:14 for X being OrtAfPl holds ( X is satisfying_TDES iff Af X is Moufangian ) proof let X be OrtAfPl; ::_thesis: ( X is satisfying_TDES iff Af X is Moufangian ) ( Af X is Moufangian implies X is satisfying_TDES ) proof assume A1: Af X is Moufangian ; ::_thesis: X is satisfying_TDES now__::_thesis:_for_o9,_a9,_a19,_b9,_b19,_c9,_c19_being_Element_of_X_st_o9_<>_a9_&_o9_<>_a19_&_o9_<>_b9_&_o9_<>_b19_&_o9_<>_c9_&_o9_<>_c19_&_not_LIN_b9,b19,a9_&_not_LIN_b9,b19,c9_&_LIN_o9,a9,a19_&_LIN_o9,b9,b19_&_LIN_o9,c9,c19_&_a9,b9_//_a19,b19_&_a9,b9_//_o9,c9_&_b9,c9_//_b19,c19_holds_ a9,c9_//_a19,c19 let o9, a9, a19, b9, b19, c9, c19 be Element of X; ::_thesis: ( o9 <> a9 & o9 <> a19 & o9 <> b9 & o9 <> b19 & o9 <> c9 & o9 <> c19 & not LIN b9,b19,a9 & not LIN b9,b19,c9 & LIN o9,a9,a19 & LIN o9,b9,b19 & LIN o9,c9,c19 & a9,b9 // a19,b19 & a9,b9 // o9,c9 & b9,c9 // b19,c19 implies a9,c9 // a19,c19 ) assume that o9 <> a9 and o9 <> a19 and A2: o9 <> b9 and o9 <> b19 and A3: o9 <> c9 and o9 <> c19 and A4: not LIN b9,b19,a9 and A5: not LIN b9,b19,c9 and A6: LIN o9,a9,a19 and A7: LIN o9,b9,b19 and A8: LIN o9,c9,c19 and A9: a9,b9 // a19,b19 and A10: a9,b9 // o9,c9 and A11: b9,c9 // b19,c19 ; ::_thesis: a9,c9 // a19,c19 reconsider o = o9, a = a9, a1 = a19, b = b9, b1 = b19, c = c9, c1 = c19 as Element of (Af X) by ANALMETR:35; A12: LIN o,b,b1 by A7, ANALMETR:40; LIN o,c,c1 by A8, ANALMETR:40; then consider M being Subset of (Af X) such that A13: M is being_line and A14: o in M and A15: c in M and A16: c1 in M by AFF_1:21; A17: not LIN b,b1,c by A5, ANALMETR:40; A18: not b in M proof LIN b,b1,o by A12, AFF_1:6; then b,b1 // b,o by AFF_1:def_1; then A19: b,b1 // o,b by AFF_1:4; assume b in M ; ::_thesis: contradiction then o,b // b,c by A13, A14, A15, AFF_1:39, AFF_1:41; then b,b1 // b,c by A2, A19, AFF_1:5; hence contradiction by A17, AFF_1:def_1; ::_thesis: verum end; a,b // a1,b1 by A9, ANALMETR:36; then A20: b,a // b1,a1 by AFF_1:4; not LIN b,b1,a by A4, ANALMETR:40; then A21: b <> a by AFF_1:7; A22: b,c // b1,c1 by A11, ANALMETR:36; A23: LIN o,a,a1 by A6, ANALMETR:40; a,b // o,c by A10, ANALMETR:36; then b,a // o,c by AFF_1:4; then b,a // M by A3, A13, A14, A15, AFF_1:27; then a,c // a1,c1 by A1, A3, A23, A12, A13, A14, A15, A16, A18, A21, A20, A22, AFF_2:def_7; hence a9,c9 // a19,c19 by ANALMETR:36; ::_thesis: verum end; hence X is satisfying_TDES by CONMETR:def_5; ::_thesis: verum end; hence ( X is satisfying_TDES iff Af X is Moufangian ) by CONMETR:7; ::_thesis: verum end; theorem :: CONMETR1:15 for X being OrtAfPl holds ( Af X is translational iff X is satisfying_des ) proof let X be OrtAfPl; ::_thesis: ( Af X is translational iff X is satisfying_des ) ( X is satisfying_des implies Af X is translational ) proof assume A1: X is satisfying_des ; ::_thesis: Af X is translational now__::_thesis:_for_A,_M,_N_being_Subset_of_(Af_X) for_a,_b,_c,_a1,_b1,_c1_being_Element_of_(Af_X)_st_A_//_M_&_A_//_N_&_a_in_A_&_a1_in_A_&_b_in_M_&_b1_in_M_&_c_in_N_&_c1_in_N_&_A_is_being_line_&_M_is_being_line_&_N_is_being_line_&_A_<>_M_&_A_<>_N_&_a,b_//_a1,b1_&_a,c_//_a1,c1_holds_ b,c_//_b1,c1 let A, M, N be Subset of (Af X); ::_thesis: for a, b, c, a1, b1, c1 being Element of (Af X) st A // M & A // N & a in A & a1 in A & b in M & b1 in M & c in N & c1 in N & A is being_line & M is being_line & N is being_line & A <> M & A <> N & a,b // a1,b1 & a,c // a1,c1 holds b,c // b1,c1 let a, b, c, a1, b1, c1 be Element of (Af X); ::_thesis: ( A // M & A // N & a in A & a1 in A & b in M & b1 in M & c in N & c1 in N & A is being_line & M is being_line & N is being_line & A <> M & A <> N & a,b // a1,b1 & a,c // a1,c1 implies b,c // b1,c1 ) assume that A2: A // M and A3: A // N and A4: a in A and A5: a1 in A and A6: b in M and A7: b1 in M and A8: c in N and A9: c1 in N and A10: A is being_line and A11: M is being_line and A12: N is being_line and A13: A <> M and A14: A <> N and A15: a,b // a1,b1 and A16: a,c // a1,c1 ; ::_thesis: b,c // b1,c1 reconsider a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1 as Element of X by ANALMETR:35; b,c // b1,c1 proof assume A17: not b,c // b1,c1 ; ::_thesis: contradiction A18: a <> a1 proof assume A19: a = a1 ; ::_thesis: contradiction A20: c = c1 proof LIN a,c,c1 by A16, A19, AFF_1:def_1; then A21: LIN c,c1,a by AFF_1:6; assume c <> c1 ; ::_thesis: contradiction then a in N by A8, A9, A12, A21, AFF_1:25; hence contradiction by A3, A4, A14, AFF_1:45; ::_thesis: verum end; b = b1 proof LIN a,b,b1 by A15, A19, AFF_1:def_1; then A22: LIN b,b1,a by AFF_1:6; assume b <> b1 ; ::_thesis: contradiction then a in M by A6, A7, A11, A22, AFF_1:25; hence contradiction by A2, A4, A13, AFF_1:45; ::_thesis: verum end; hence contradiction by A17, A20, AFF_1:2; ::_thesis: verum end; A23: ( not LIN a9,a19,b9 & not LIN a9,a19,c9 ) proof assume ( LIN a9,a19,b9 or LIN a9,a19,c9 ) ; ::_thesis: contradiction then ( LIN a,a1,b or LIN a,a1,c ) by ANALMETR:40; then ( b in A or c in A ) by A4, A5, A10, A18, AFF_1:25; hence contradiction by A2, A3, A6, A8, A13, A14, AFF_1:45; ::_thesis: verum end; a,a1 // c,c1 by A3, A4, A5, A8, A9, AFF_1:39; then A24: a9,a19 // c9,c19 by ANALMETR:36; a,a1 // b,b1 by A2, A4, A5, A6, A7, AFF_1:39; then A25: a9,a19 // b9,b19 by ANALMETR:36; A26: a9,c9 // a19,c19 by A16, ANALMETR:36; a9,b9 // a19,b19 by A15, ANALMETR:36; then b9,c9 // b19,c19 by A1, A23, A25, A24, A26, CONMETR:def_8; hence contradiction by A17, ANALMETR:36; ::_thesis: verum end; hence b,c // b1,c1 ; ::_thesis: verum end; hence Af X is translational by AFF_2:def_11; ::_thesis: verum end; hence ( Af X is translational iff X is satisfying_des ) by CONMETR:8; ::_thesis: verum end; theorem :: CONMETR1:16 for X being OrtAfPl holds ( X is satisfying_PAP iff Af X is Pappian ) proof let X be OrtAfPl; ::_thesis: ( X is satisfying_PAP iff Af X is Pappian ) A1: ( X is satisfying_PAP implies Af X is Pappian ) proof assume A2: X is satisfying_PAP ; ::_thesis: Af X is Pappian now__::_thesis:_for_M,_N_being_Subset_of_(Af_X) for_o,_a,_b,_c,_a1,_b1,_c1_being_Element_of_(Af_X)_st_M_is_being_line_&_N_is_being_line_&_M_<>_N_&_o_in_M_&_o_in_N_&_o_<>_a_&_o_<>_a1_&_o_<>_b_&_o_<>_b1_&_o_<>_c_&_o_<>_c1_&_a_in_M_&_b_in_M_&_c_in_M_&_a1_in_N_&_b1_in_N_&_c1_in_N_&_a,b1_//_b,a1_&_b,c1_//_c,b1_holds_ a,c1_//_c,a1 let M, N be Subset of (Af X); ::_thesis: for o, a, b, c, a1, b1, c1 being Element of (Af X) st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a in M & b in M & c in M & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 holds a,c1 // c,a1 let o, a, b, c, a1, b1, c1 be Element of (Af X); ::_thesis: ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a in M & b in M & c in M & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 implies a,c1 // c,a1 ) assume that A3: M is being_line and A4: N is being_line and A5: M <> N and A6: o in M and A7: o in N and A8: o <> a and A9: o <> a1 and A10: o <> b and A11: o <> b1 and A12: o <> c and A13: o <> c1 and A14: a in M and A15: b in M and A16: c in M and A17: a1 in N and A18: b1 in N and A19: c1 in N and A20: a,b1 // b,a1 and A21: b,c1 // c,b1 ; ::_thesis: a,c1 // c,a1 reconsider a9 = a, b9 = b, c9 = c, a19 = a1, b19 = b1, c19 = c1 as Element of X by ANALMETR:35; reconsider M9 = M, N9 = N as Subset of X by ANALMETR:42; A22: N9 is being_line by A4, ANALMETR:43; A23: ( not c19 in M9 & not b9 in N9 ) proof assume ( c19 in M9 or b9 in N9 ) ; ::_thesis: contradiction then A24: ( o,c1 // M or o,b // N ) by A3, A4, A6, A7, AFF_1:52; A25: o,b // M by A3, A6, A15, AFF_1:52; o,c1 // N by A4, A7, A19, AFF_1:52; hence contradiction by A5, A6, A7, A10, A13, A24, A25, AFF_1:45, AFF_1:53; ::_thesis: verum end; b,a1 // a,b1 by A20, AFF_1:4; then A26: b9,a19 // a9,b19 by ANALMETR:36; A27: b9,c19 // c9,b19 by A21, ANALMETR:36; M9 is being_line by A3, ANALMETR:43; then a9,c19 // c9,a19 by A2, A6, A7, A8, A9, A11, A12, A14, A15, A16, A17, A18, A19, A22, A26, A27, A23, CONMETR:def_2; hence a,c1 // c,a1 by ANALMETR:36; ::_thesis: verum end; hence Af X is Pappian by AFF_2:def_2; ::_thesis: verum end; ( Af X is Pappian implies X is satisfying_PAP ) proof assume A28: Af X is Pappian ; ::_thesis: X is satisfying_PAP now__::_thesis:_for_o9,_a19,_a29,_a39,_b19,_b29,_b39_being_Element_of_X for_M9,_N9_being_Subset_of_X_st_M9_is_being_line_&_N9_is_being_line_&_o9_in_M9_&_a19_in_M9_&_a29_in_M9_&_a39_in_M9_&_o9_in_N9_&_b19_in_N9_&_b29_in_N9_&_b39_in_N9_&_not_b29_in_M9_&_not_a39_in_N9_&_o9_<>_a19_&_o9_<>_a29_&_o9_<>_a39_&_o9_<>_b19_&_o9_<>_b29_&_o9_<>_b39_&_a39,b29_//_a29,b19_&_a39,b39_//_a19,b19_holds_ a19,b29_//_a29,b39 let o9, a19, a29, a39, b19, b29, b39 be Element of X; ::_thesis: for M9, N9 being Subset of X st M9 is being_line & N9 is being_line & o9 in M9 & a19 in M9 & a29 in M9 & a39 in M9 & o9 in N9 & b19 in N9 & b29 in N9 & b39 in N9 & not b29 in M9 & not a39 in N9 & o9 <> a19 & o9 <> a29 & o9 <> a39 & o9 <> b19 & o9 <> b29 & o9 <> b39 & a39,b29 // a29,b19 & a39,b39 // a19,b19 holds a19,b29 // a29,b39 let M9, N9 be Subset of X; ::_thesis: ( M9 is being_line & N9 is being_line & o9 in M9 & a19 in M9 & a29 in M9 & a39 in M9 & o9 in N9 & b19 in N9 & b29 in N9 & b39 in N9 & not b29 in M9 & not a39 in N9 & o9 <> a19 & o9 <> a29 & o9 <> a39 & o9 <> b19 & o9 <> b29 & o9 <> b39 & a39,b29 // a29,b19 & a39,b39 // a19,b19 implies a19,b29 // a29,b39 ) assume that A29: M9 is being_line and A30: N9 is being_line and A31: o9 in M9 and A32: a19 in M9 and A33: a29 in M9 and A34: a39 in M9 and A35: o9 in N9 and A36: b19 in N9 and A37: b29 in N9 and A38: b39 in N9 and A39: not b29 in M9 and A40: not a39 in N9 and A41: o9 <> a19 and A42: o9 <> a29 and o9 <> a39 and A43: o9 <> b19 and o9 <> b29 and A44: o9 <> b39 and A45: a39,b29 // a29,b19 and A46: a39,b39 // a19,b19 ; ::_thesis: a19,b29 // a29,b39 reconsider a1 = a19, a2 = a29, a3 = a39, b1 = b19, b2 = b29, b3 = b39 as Element of (Af X) by ANALMETR:35; reconsider M = M9, N = N9 as Subset of (Af X) by ANALMETR:42; A47: N is being_line by A30, ANALMETR:43; A48: M is being_line by A29, ANALMETR:43; now__::_thesis:_(_M_<>_N_implies_a19,b29_//_a29,b39_) assume M <> N ; ::_thesis: a19,b29 // a29,b39 a3,b3 // a1,b1 by A46, ANALMETR:36; then A49: a1,b1 // a3,b3 by AFF_1:4; a3,b2 // a2,b1 by A45, ANALMETR:36; then a1,b2 // a2,b3 by A28, A31, A32, A33, A34, A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A48, A47, A49, AFF_2:def_2; hence a19,b29 // a29,b39 by ANALMETR:36; ::_thesis: verum end; hence a19,b29 // a29,b39 by A37, A39; ::_thesis: verum end; hence X is satisfying_PAP by CONMETR:def_2; ::_thesis: verum end; hence ( X is satisfying_PAP iff Af X is Pappian ) by A1; ::_thesis: verum end; theorem :: CONMETR1:17 for X being OrtAfPl holds ( X is satisfying_DES iff Af X is Desarguesian ) proof let X be OrtAfPl; ::_thesis: ( X is satisfying_DES iff Af X is Desarguesian ) A1: ( X is satisfying_DES implies Af X is Desarguesian ) proof assume A2: X is satisfying_DES ; ::_thesis: Af X is Desarguesian now__::_thesis:_for_A,_M,_N_being_Subset_of_(Af_X) for_o,_a,_b,_c,_a1,_b1,_c1_being_Element_of_(Af_X)_st_o_in_A_&_o_in_M_&_o_in_N_&_o_<>_a_&_o_<>_b_&_o_<>_c_&_a_in_A_&_a1_in_A_&_b_in_M_&_b1_in_M_&_c_in_N_&_c1_in_N_&_A_is_being_line_&_M_is_being_line_&_N_is_being_line_&_A_<>_M_&_A_<>_N_&_a,b_//_a1,b1_&_a,c_//_a1,c1_holds_ b,c_//_b1,c1 let A, M, N be Subset of (Af X); ::_thesis: for o, a, b, c, a1, b1, c1 being Element of (Af X) st o in A & o in M & o in N & o <> a & o <> b & o <> c & a in A & a1 in A & b in M & b1 in M & c in N & c1 in N & A is being_line & M is being_line & N is being_line & A <> M & A <> N & a,b // a1,b1 & a,c // a1,c1 holds b,c // b1,c1 let o, a, b, c, a1, b1, c1 be Element of (Af X); ::_thesis: ( o in A & o in M & o in N & o <> a & o <> b & o <> c & a in A & a1 in A & b in M & b1 in M & c in N & c1 in N & A is being_line & M is being_line & N is being_line & A <> M & A <> N & a,b // a1,b1 & a,c // a1,c1 implies b,c // b1,c1 ) assume that A3: o in A and A4: o in M and A5: o in N and A6: o <> a and A7: o <> b and A8: o <> c and A9: a in A and A10: a1 in A and A11: b in M and A12: b1 in M and A13: c in N and A14: c1 in N and A15: A is being_line and A16: M is being_line and A17: N is being_line and A18: A <> M and A19: A <> N and A20: a,b // a1,b1 and A21: a,c // a1,c1 ; ::_thesis: b,c // b1,c1 reconsider o9 = o, a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1 as Element of X by ANALMETR:35; o,b // o,b1 by A4, A11, A12, A16, AFF_1:39, AFF_1:41; then A22: LIN o,b,b1 by AFF_1:def_1; then A23: LIN o9,b9,b19 by ANALMETR:40; o,a // o,a1 by A3, A9, A10, A15, AFF_1:39, AFF_1:41; then A24: LIN o,a,a1 by AFF_1:def_1; o,c // o,c1 by A5, A13, A14, A17, AFF_1:39, AFF_1:41; then A25: LIN o,c,c1 by AFF_1:def_1; then A26: LIN o9,c9,c19 by ANALMETR:40; assume A27: not b,c // b1,c1 ; ::_thesis: contradiction A28: ( not LIN b9,b19,a9 & not LIN a9,a19,c9 ) proof A29: a <> a1 proof assume A30: a = a1 ; ::_thesis: contradiction A31: c = c1 proof A32: not LIN o,a,c proof assume LIN o,a,c ; ::_thesis: contradiction then c in A by A3, A6, A9, A15, AFF_1:25; then A33: o,c // A by A3, A15, AFF_1:52; o,c // N by A5, A13, A17, AFF_1:52; hence contradiction by A3, A5, A8, A19, A33, AFF_1:45, AFF_1:53; ::_thesis: verum end; assume c <> c1 ; ::_thesis: contradiction hence contradiction by A21, A25, A30, A32, AFF_1:14; ::_thesis: verum end; b = b1 proof A34: not LIN o,a,b proof assume LIN o,a,b ; ::_thesis: contradiction then b in A by A3, A6, A9, A15, AFF_1:25; then A35: o,b // A by A3, A15, AFF_1:52; o,b // M by A4, A11, A16, AFF_1:52; hence contradiction by A3, A4, A7, A18, A35, AFF_1:45, AFF_1:53; ::_thesis: verum end; assume b <> b1 ; ::_thesis: contradiction hence contradiction by A20, A22, A30, A34, AFF_1:14; ::_thesis: verum end; hence contradiction by A27, A31, AFF_1:2; ::_thesis: verum end; A36: b <> b1 proof A37: not LIN o,b,a proof assume LIN o,b,a ; ::_thesis: contradiction then a in M by A4, A7, A11, A16, AFF_1:25; then A38: o,a // M by A4, A16, AFF_1:52; o,a // A by A3, A9, A15, AFF_1:52; hence contradiction by A3, A4, A6, A18, A38, AFF_1:45, AFF_1:53; ::_thesis: verum end; assume b = b1 ; ::_thesis: contradiction then b,a // b,a1 by A20, AFF_1:4; hence contradiction by A24, A29, A37, AFF_1:14; ::_thesis: verum end; assume ( LIN b9,b19,a9 or LIN a9,a19,c9 ) ; ::_thesis: contradiction then ( LIN b,b1,a or LIN a,a1,c ) by ANALMETR:40; then ( a in M or c in A ) by A9, A10, A11, A12, A15, A16, A29, A36, AFF_1:25; then A39: ( o,a // M or o,c // A ) by A3, A4, A15, A16, AFF_1:52; A40: o,c // N by A5, A13, A17, AFF_1:52; o,a // A by A3, A9, A15, AFF_1:52; hence contradiction by A3, A4, A5, A6, A8, A18, A19, A39, A40, AFF_1:45, AFF_1:53; ::_thesis: verum end; A41: a9,c9 // a19,c19 by A21, ANALMETR:36; A42: a9,b9 // a19,b19 by A20, ANALMETR:36; A43: ( o9 <> a19 & o9 <> b19 & o9 <> c19 ) proof A44: now__::_thesis:_not_o9_=_a19 assume A45: o9 = a19 ; ::_thesis: contradiction A46: o = c1 proof A47: not LIN c,a,o proof assume LIN c,a,o ; ::_thesis: contradiction then LIN o,a,c by AFF_1:6; then c in A by A3, A6, A9, A15, AFF_1:25; then A48: o,c // A by A3, A15, AFF_1:52; o,c // N by A5, A13, A17, AFF_1:52; hence contradiction by A3, A5, A8, A19, A48, AFF_1:45, AFF_1:53; ::_thesis: verum end; assume A49: o <> c1 ; ::_thesis: contradiction A50: o,c // o,c1 by A5, A13, A14, A17, AFF_1:39, AFF_1:41; then a,c // o,c by A21, A45, A49, AFF_1:5; then c,a // c,o by AFF_1:4; then LIN c,a,o by AFF_1:def_1; then LIN o,a,c by AFF_1:6; then o,a // o,c by AFF_1:def_1; then o,a // o,c1 by A8, A50, AFF_1:5; then LIN o,a,c1 by AFF_1:def_1; then LIN a,o,c1 by AFF_1:6; then A51: a,o // a,c1 by AFF_1:def_1; LIN c,o,c1 by A25, AFF_1:6; hence contradiction by A49, A47, A51, AFF_1:14; ::_thesis: verum end; o = b1 proof A52: not LIN b,a,o proof assume LIN b,a,o ; ::_thesis: contradiction then LIN o,a,b by AFF_1:6; then b in A by A3, A6, A9, A15, AFF_1:25; then A53: o,b // A by A3, A15, AFF_1:52; o,b // M by A4, A11, A16, AFF_1:52; hence contradiction by A3, A4, A7, A18, A53, AFF_1:45, AFF_1:53; ::_thesis: verum end; assume A54: o <> b1 ; ::_thesis: contradiction A55: o,b1 // o,b by A4, A11, A12, A16, AFF_1:39, AFF_1:41; then a,b // o,b by A20, A45, A54, AFF_1:5; then b,a // b,o by AFF_1:4; then LIN b,a,o by AFF_1:def_1; then LIN o,a,b by AFF_1:6; then o,a // o,b by AFF_1:def_1; then o,a // o,b1 by A7, A55, AFF_1:5; then LIN o,a,b1 by AFF_1:def_1; then LIN a,o,b1 by AFF_1:6; then A56: a,o // a,b1 by AFF_1:def_1; LIN b,o,b1 by A22, AFF_1:6; hence contradiction by A54, A52, A56, AFF_1:14; ::_thesis: verum end; hence contradiction by A27, A46, AFF_1:3; ::_thesis: verum end; A57: now__::_thesis:_not_o9_=_b19 A58: not LIN a,b,o proof assume LIN a,b,o ; ::_thesis: contradiction then LIN o,a,b by AFF_1:6; then b in A by A3, A6, A9, A15, AFF_1:25; then A59: o,b // A by A3, A15, AFF_1:52; o,b // M by A4, A11, A16, AFF_1:52; hence contradiction by A3, A4, A7, A18, A59, AFF_1:45, AFF_1:53; ::_thesis: verum end; A60: a1,o // a,o by A3, A9, A10, A15, AFF_1:39, AFF_1:41; assume o9 = b19 ; ::_thesis: contradiction then a,b // a,o by A20, A44, A60, AFF_1:5; then LIN a,b,o by AFF_1:def_1; then LIN o,b,a by AFF_1:6; then o,b // o,a by AFF_1:def_1; then o,b // a,o by AFF_1:4; then o,b // a1,o by A6, A60, AFF_1:5; then o,b // o,a1 by AFF_1:4; then LIN o,b,a1 by AFF_1:def_1; then LIN b,o,a1 by AFF_1:6; then A61: b,o // b,a1 by AFF_1:def_1; LIN a,o,a1 by A24, AFF_1:6; hence contradiction by A44, A58, A61, AFF_1:14; ::_thesis: verum end; A62: now__::_thesis:_not_o9_=_c19 A63: not LIN a,c,o proof assume LIN a,c,o ; ::_thesis: contradiction then LIN o,a,c by AFF_1:6; then c in A by A3, A6, A9, A15, AFF_1:25; then A64: o,c // A by A3, A15, AFF_1:52; o,c // N by A5, A13, A17, AFF_1:52; hence contradiction by A3, A5, A8, A19, A64, AFF_1:45, AFF_1:53; ::_thesis: verum end; A65: a1,o // a,o by A3, A9, A10, A15, AFF_1:39, AFF_1:41; assume o9 = c19 ; ::_thesis: contradiction then a,c // a,o by A21, A44, A65, AFF_1:5; then LIN a,c,o by AFF_1:def_1; then LIN o,c,a by AFF_1:6; then o,c // o,a by AFF_1:def_1; then o,c // a,o by AFF_1:4; then o,c // a1,o by A6, A65, AFF_1:5; then o,c // o,a1 by AFF_1:4; then LIN o,c,a1 by AFF_1:def_1; then LIN c,o,a1 by AFF_1:6; then A66: c,o // c,a1 by AFF_1:def_1; LIN a,o,a1 by A24, AFF_1:6; hence contradiction by A44, A63, A66, AFF_1:14; ::_thesis: verum end; assume ( not o9 <> a19 or not o9 <> b19 or not o9 <> c19 ) ; ::_thesis: contradiction hence contradiction by A44, A57, A62; ::_thesis: verum end; LIN o9,a9,a19 by A24, ANALMETR:40; then b9,c9 // b19,c19 by A2, A6, A7, A8, A23, A26, A43, A28, A42, A41, CONAFFM:def_1; hence contradiction by A27, ANALMETR:36; ::_thesis: verum end; hence Af X is Desarguesian by AFF_2:def_4; ::_thesis: verum end; ( Af X is Desarguesian implies X is satisfying_DES ) proof assume A67: Af X is Desarguesian ; ::_thesis: X is satisfying_DES now__::_thesis:_for_o9,_a9,_a19,_b9,_b19,_c9,_c19_being_Element_of_X_st_o9_<>_a9_&_o9_<>_a19_&_o9_<>_b9_&_o9_<>_b19_&_o9_<>_c9_&_o9_<>_c19_&_not_LIN_b9,b19,a9_&_not_LIN_a9,a19,c9_&_LIN_o9,a9,a19_&_LIN_o9,b9,b19_&_LIN_o9,c9,c19_&_a9,b9_//_a19,b19_&_a9,c9_//_a19,c19_holds_ b9,c9_//_b19,c19 let o9, a9, a19, b9, b19, c9, c19 be Element of X; ::_thesis: ( o9 <> a9 & o9 <> a19 & o9 <> b9 & o9 <> b19 & o9 <> c9 & o9 <> c19 & not LIN b9,b19,a9 & not LIN a9,a19,c9 & LIN o9,a9,a19 & LIN o9,b9,b19 & LIN o9,c9,c19 & a9,b9 // a19,b19 & a9,c9 // a19,c19 implies b9,c9 // b19,c19 ) assume that A68: o9 <> a9 and o9 <> a19 and A69: o9 <> b9 and o9 <> b19 and A70: o9 <> c9 and o9 <> c19 and A71: not LIN b9,b19,a9 and A72: not LIN a9,a19,c9 and A73: LIN o9,a9,a19 and A74: LIN o9,b9,b19 and A75: LIN o9,c9,c19 and A76: a9,b9 // a19,b19 and A77: a9,c9 // a19,c19 ; ::_thesis: b9,c9 // b19,c19 reconsider o = o9, a = a9, a1 = a19, b = b9, b1 = b19, c = c9, c1 = c19 as Element of (Af X) by ANALMETR:35; A78: not LIN a,a1,c by A72, ANALMETR:40; A79: a,c // a1,c1 by A77, ANALMETR:36; A80: a,b // a1,b1 by A76, ANALMETR:36; LIN o,b,b1 by A74, ANALMETR:40; then consider M being Subset of (Af X) such that A81: M is being_line and A82: o in M and A83: b in M and A84: b1 in M by AFF_1:21; LIN o,c,c1 by A75, ANALMETR:40; then consider N being Subset of (Af X) such that A85: N is being_line and A86: o in N and A87: c in N and A88: c1 in N by AFF_1:21; LIN o,a,a1 by A73, ANALMETR:40; then consider A being Subset of (Af X) such that A89: A is being_line and A90: o in A and A91: a in A and A92: a1 in A by AFF_1:21; A93: not LIN b,b1,a by A71, ANALMETR:40; ( A <> M & A <> N ) proof assume ( not A <> M or not A <> N ) ; ::_thesis: contradiction then ( b,b1 // b,a or a,a1 // a,c ) by A89, A91, A92, A83, A84, A87, AFF_1:39, AFF_1:41; hence contradiction by A93, A78, AFF_1:def_1; ::_thesis: verum end; then b,c // b1,c1 by A67, A68, A69, A70, A89, A90, A91, A92, A81, A82, A83, A84, A85, A86, A87, A88, A80, A79, AFF_2:def_4; hence b9,c9 // b19,c19 by ANALMETR:36; ::_thesis: verum end; hence X is satisfying_DES by CONAFFM:def_1; ::_thesis: verum end; hence ( X is satisfying_DES iff Af X is Desarguesian ) by A1; ::_thesis: verum end;