:: 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;