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

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 A2: ( 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 ) ; :: thesis: a3,a4 // b3,b4
then A3: not M // N by AFF_1:59;
A4: ( M // M & N // N ) by A2, AFF_1:55;

A5: now

assume A6: ( a1 = a3 or a2 = a4 ) ; :: thesis: a3,a4 // b3,b4

A7: now

assume A8: a1 = a3 ; :: thesis: a3,a4 // b3,b4
A9: not LIN o,b2,b1 by A2, AFF_1:39;
o,b1 // o,b3 by A2, A4, AFF_1:53;
then A10: LIN o,b1,b3 by AFF_1:def 1;
b2,b1 // b2,b3

proof

a2,a1 // b2,b3 by A2, A8, AFF_1:13;
hence b2,b1 // b2,b3 by A2, AFF_1:14; :: thesis: verum

end;

hence a3,a4 // b3,b4 by A2, A8, A9, A10, AFF_1:23; :: thesis: verum

end;

now

assume A11: a2 = a4 ; :: thesis: a3,a4 // b3,b4
A12: not LIN o,b1,b2 by A2, AFF_1:39;
o,b2 // o,b4 by A2, A4, AFF_1:53;
then A13: LIN o,b2,b4 by AFF_1:def 1;
b1,b2 // b1,b4

proof

a1,a4 // b1,b2 by A2, A11, AFF_1:13;
hence b1,b2 // b1,b4 by A2, AFF_1:14; :: thesis: verum

end;

hence a3,a4 // b3,b4 by A2, A11, A12, A13, AFF_1:23; :: thesis: verum

end;

hence a3,a4 // b3,b4 by A6, A7; :: thesis: verum

end;

now

assume A14: ( a1 <> a3 & a2 <> a4 ) ; :: thesis: a3,a4 // b3,b4
consider d1 being Element of X such that
A15: ( o <> d1 & d1 in N ) by A2;
ex d2 being Element of X st
( d2 in M & a2,a1 // d2,d1 )

proof

consider e1 being Element of X such that
A16: ( o <> e1 & e1 in M ) by A2;
consider e2 being Element of X such that
A17: ( a2,a1 // d1,e2 & d1 <> e2 ) by DIRAF:47;
not o,e1 // d1,e2

proof

assume o,e1 // d1,e2 ; :: thesis: contradiction
then A18: o,e1 // a2,a1 by A17, AFF_1:14;
o,e1 // a1,a3 by A2, A4, A16, AFF_1:53;
then a1,a3 // a2,a1 by A16, A18, AFF_1:14;
then a1,a3 // a1,a2 by AFF_1:13;
then LIN a1,a3,a2 by AFF_1:def 1;
hence contradiction by A2, A14, AFF_1:39; :: thesis: verum

end;

then consider d2 being Element of X such that
A19: ( LIN o,e1,d2 & LIN d1,e2,d2 ) by AFF_1:74;
take d2 ; :: thesis: ( d2 in M & a2,a1 // d2,d1 )
d1,e2 // d1,d2 by A19, AFF_1:def 1;
then a2,a1 // d1,d2 by A17, AFF_1:14;
hence ( d2 in M & a2,a1 // d2,d1 ) by A2, A16, A19, AFF_1:13, AFF_1:39; :: thesis: verum

end;

then consider d2 being Element of X such that
A20: ( d2 in M & a2,a1 // d2,d1 ) ;
ex d3 being Element of X st
( d3 in N & a3,a2 // d3,d2 )

proof

consider e1 being Element of X such that
A21: ( o <> e1 & e1 in N ) by A2;
consider e2 being Element of X such that
A22: ( a3,a2 // d2,e2 & d2 <> e2 ) by DIRAF:47;
not o,e1 // d2,e2

proof

assume o,e1 // d2,e2 ; :: thesis: contradiction
then A23: o,e1 // a3,a2 by A22, AFF_1:14;
o,e1 // a2,a4 by A2, A4, A21, AFF_1:53;
then a2,a4 // a3,a2 by A21, A23, AFF_1:14;
then a2,a4 // a2,a3 by AFF_1:13;
then LIN a2,a4,a3 by AFF_1:def 1;
hence contradiction by A2, A14, AFF_1:39; :: thesis: verum

end;

then consider d3 being Element of X such that
A24: ( LIN o,e1,d3 & LIN d2,e2,d3 ) by AFF_1:74;
take d3 ; :: thesis: ( d3 in N & a3,a2 // d3,d2 )
d2,e2 // d2,d3 by A24, AFF_1:def 1;
then a3,a2 // d2,d3 by A22, AFF_1:14;
hence ( d3 in N & a3,a2 // d3,d2 ) by A2, A21, A24, AFF_1:13, AFF_1:39; :: thesis: verum

end;

then consider d3 being Element of X such that
A25: ( d3 in N & a3,a2 // d3,d2 ) ;
ex d4 being Element of X st
( d4 in M & a1,a4 // d1,d4 )

proof

consider e1 being Element of X such that
A26: ( o <> e1 & e1 in M ) by A2;
consider e2 being Element of X such that
A27: ( a1,a4 // d1,e2 & d1 <> e2 ) by DIRAF:47;
not o,e1 // d1,e2

proof

assume o,e1 // d1,e2 ; :: thesis: contradiction
then A28: o,e1 // a1,a4 by A27, AFF_1:14;
o,e1 // a1,a3 by A2, A4, A26, AFF_1:53;
then a1,a3 // a1,a4 by A26, A28, AFF_1:14;
then LIN a1,a3,a4 by AFF_1:def 1;
hence contradiction by A2, A14, AFF_1:39; :: thesis: verum

end;

then consider d4 being Element of X such that
A29: ( LIN o,e1,d4 & LIN d1,e2,d4 ) by AFF_1:74;
take d4 ; :: thesis: ( d4 in M & a1,a4 // d1,d4 )
d1,e2 // d1,d4 by A29, AFF_1:def 1;
hence ( d4 in M & a1,a4 // d1,d4 ) by A2, A26, A27, A29, AFF_1:14, AFF_1:39; :: thesis: verum

end;

then consider d4 being Element of X such that
A30: ( d4 in M & a1,a4 // d1,d4 ) ;
A31: ( d2 <> o & d3 <> o & d4 <> o )

proof

assume A32: ( not d2 <> o or not d3 <> o or not d4 <> o ) ; :: thesis: contradiction

A33: now

assume A34: d2 = o ; :: thesis: contradiction
o,d1 // a2,a4 by A2, A4, A15, AFF_1:53;
then a2,a4 // a2,a1 by A15, A20, A34, AFF_1:14;
then LIN a2,a4,a1 by AFF_1:def 1;
hence contradiction by A2, A14, AFF_1:39; :: thesis: verum

end;

A35: now

assume A36: d3 = o ; :: thesis: contradiction
o,d2 // a3,a1 by A2, A4, A20, AFF_1:53;
then a3,a1 // a3,a2 by A25, A33, A36, AFF_1:14;
then LIN a3,a1,a2 by AFF_1:def 1;
hence contradiction by A2, A14, AFF_1:39; :: thesis: verum

end;

now

assume A37: d4 = o ; :: thesis: contradiction
d1,o // a2,a4 by A2, A4, A15, AFF_1:53;
then a1,a4 // a2,a4 by A15, A30, A37, AFF_1:14;
then a4,a2 // a4,a1 by AFF_1:13;
then LIN a4,a2,a1 by AFF_1:def 1;
hence contradiction by A2, A14, AFF_1:39; :: thesis: verum

end;

hence contradiction by A32, A33, A35; :: thesis: verum

end;

A38: ( 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 A39: ( o,d1 // M or o,d3 // M or o,d2 // N or o,d4 // N ) by A2, AFF_1:66;
( o,d1 // N & o,d3 // N & o,d2 // M & o,d4 // M ) by A2, A15, A20, A25, A30, AFF_1:66;
hence contradiction by A3, A15, A31, A39, AFF_1:67; :: thesis: verum

end;

then A40: a3,a4 // d3,d4 by A1, A2, A15, A20, A25, A30, Def6;
A41: ( 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 A42: ( o,d1 // M or o,d3 // M ) by A2, A20, A30, AFF_1:66;
( o,d1 // N & o,d3 // N ) by A2, A15, A25, AFF_1:66;
hence contradiction by A3, A15, A31, A42, AFF_1:67; :: thesis: verum

end;

A43: b2,b1 // d2,d1 by A2, A20, AFF_1:14;
A44: b3,b2 // d3,d2 by A2, A25, AFF_1:14;
b1,b4 // d1,d4 by A2, A30, AFF_1:14;
then b3,b4 // d3,d4 by A1, A2, A15, A20, A25, A30, A38, A43, A44, Def6;
hence a3,a4 // b3,b4 by A40, A41, AFF_1:14; :: thesis: verum

end;

hence a3,a4 // b3,b4 by A5; :: thesis: verum

end;

hence X is satisfying_major_Scherungssatz by Def2; :: thesis: verum