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