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

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: ( M // M & N // N ) by AFF_1:55;

A4: now

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

A6: now

assume A7: a1 = a3 ; :: thesis: a3,a4 // b3,b4
A8: not LIN o,b2,b1 by A2, AFF_1:39;
o,b1 // o,b3 by A2, A3, AFF_1:53;
then A9: LIN o,b1,b3 by AFF_1:def 1;
a2,a1 // b2,b3 by A2, A7, AFF_1:13;
then b2,b1 // b2,b3 by A2, AFF_1:14;
hence a3,a4 // b3,b4 by A2, A7, A8, A9, AFF_1:23; :: thesis: verum

end;

now

assume A10: a2 = a4 ; :: thesis: a3,a4 // b3,b4
A11: not LIN o,b1,b2 by A2, AFF_1:39;
o,b2 // o,b4 by A2, A3, AFF_1:53;
then A12: LIN o,b2,b4 by AFF_1:def 1;
a1,a2 // b1,b2 by A2, AFF_1:13;
then b1,b2 // b1,b4 by A2, A10, AFF_1:14;
hence a3,a4 // b3,b4 by A2, A10, A11, A12, AFF_1:23; :: thesis: verum

end;

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

end;

now

assume A13: ( a1 <> a3 & a2 <> a4 ) ; :: thesis: a3,a4 // b3,b4

A14: now

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
A15: ( LIN a1,a2,d & a1 <> d & a2 <> d ) by A2, TRANSLAC:2;
LIN o,d,d by AFF_1:16;
then consider Y being Subset of X such that
A16: ( Y is being_line & o in Y & d in Y & d in Y ) by AFF_1:33;
ex d1 being Element of X st
( LIN b1,b2,d1 & d1 in Y )

proof

not b1,b2 // o,d

proof

assume b1,b2 // o,d ; :: thesis: contradiction
then b2,b1 // o,d by AFF_1:13;
then A17: a2,a1 // o,d by A2, AFF_1:14;
LIN a2,a1,d by A15, AFF_1:15;
then a2,a1 // a2,d by AFF_1:def 1;
then a2,d // o,d by A2, A17, AFF_1:14;
then d,a2 // d,o by AFF_1:13;
then LIN d,a2,o by AFF_1:def 1;
then LIN o,d,a2 by AFF_1:15;
then A18: o,d // o,a2 by AFF_1:def 1;
A19: o <> d

proof

assume o = d ; :: thesis: contradiction
then LIN o,a1,a2 by A15, AFF_1:15;
hence contradiction by A2, AFF_1:39; :: thesis: verum

end;

then A20: Y // N by A2, A16, A18, AFF_1:52;
a1,a2 // a1,d by A15, AFF_1:def 1;
then a2,a1 // a1,d by AFF_1:13;
then a1,d // o,d by A2, A17, AFF_1:14;
then d,o // d,a1 by AFF_1:13;
then LIN d,o,a1 by AFF_1:def 1;
then LIN o,d,a1 by AFF_1:15;
then o,d // o,a1 by AFF_1:def 1;
then Y // M by A2, A16, A19, AFF_1:52;
then M // N by A20, AFF_1:58;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

then consider d1 being Element of X such that
A21: ( LIN b1,b2,d1 & LIN o,d,d1 ) by AFF_1:74;
take d1 ; :: thesis: ( LIN b1,b2,d1 & d1 in Y )
o <> d

proof

assume o = d ; :: thesis: contradiction
then LIN o,a1,a2 by A15, AFF_1:15;
hence contradiction by A2, AFF_1:39; :: thesis: verum

end;

hence ( LIN b1,b2,d1 & d1 in Y ) by A16, A21, AFF_1:39; :: thesis: verum

end;

then consider d1 being Element of X such that
A22: ( LIN b1,b2,d1 & d1 in Y ) ;
A23: o <> d

proof

assume o = d ; :: thesis: contradiction
then LIN o,a1,a2 by A15, AFF_1:15;
hence contradiction by A2, AFF_1:39; :: thesis: verum

end;

A24: ( N <> M & N <> Y & M <> Y )

proof

assume A25: ( not N <> M or not N <> Y or not M <> Y ) ; :: thesis: contradiction

now

assume A26: ( N = Y or M = Y ) ; :: thesis: contradiction
( LIN a2,d,a1 & LIN a1,d,a2 ) by A15, AFF_1:15;
hence contradiction by A2, A15, A16, A26, AFF_1:39; :: thesis: verum

end;

hence contradiction by A2, A25; :: thesis: verum

end;

A27: a2,d // b2,d1

proof

( LIN a2,a1,d & LIN b2,b1,d1 ) by A15, A22, AFF_1:15;
then A28: ( a2,a1 // a2,d & b2,b1 // b2,d1 ) by AFF_1:def 1;
then b2,b1 // a2,d by A2, AFF_1:14;
hence a2,d // b2,d1 by A2, A28, AFF_1:14; :: thesis: verum

end;

a2,a3 // b2,b3 by A2, AFF_1:13;
then A29: d,a3 // d1,b3 by A1, A2, A16, A22, A23, A24, A27, AFF_2:def 4;
a1,d // b1,d1

proof

( a1,a2 // a1,d & b1,b2 // b1,d1 ) by A15, A22, AFF_1:def 1;
then A30: ( a2,a1 // a1,d & b2,b1 // b1,d1 ) by AFF_1:13;
then b2,b1 // a1,d by A2, AFF_1:14;
hence a1,d // b1,d1 by A2, A30, AFF_1:14; :: thesis: verum

end;

then d,a4 // d1,b4 by A1, A2, A16, A22, A23, A24, AFF_2:def 4;
hence a3,a4 // b3,b4 by A1, A2, A16, A22, A23, A24, A29, AFF_2:def 4; :: thesis: verum

end;

now

assume A31: 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
A32: LIN a1,a3,b1 by A2, AFF_1:33;

A33: now

assume A34: a1 = b1 ; :: thesis: a3,a4 // b3,b4
A35: LIN a1,a3,b3 by A2, AFF_1:33;
a1 <> b3

proof

assume A36: a1 = b3 ; :: thesis: contradiction
A37: not LIN o,a2,a1 by A2, AFF_1:39;
A38: LIN o,a1,a3 by A2, AFF_1:33;
b2,b1 // a2,a3 by A2, A34, A36, AFF_1:13;
then a2,a1 // a2,a3 by A2, AFF_1:14;
hence contradiction by A13, A37, A38, AFF_1:23; :: thesis: verum

end;

then A39: a3 = b3 by A13, A31, A35;
LIN a2,a4,b4 by A2, AFF_1:33;
then A40: ( a2 = b4 or a4 = b4 ) by A13, A31;
a2 <> b4

proof

assume a2 = b4 ; :: thesis: contradiction
then LIN a1,a4,a2 by A2, A34, AFF_1:def 1;
then LIN a2,a4,a1 by AFF_1:15;
hence contradiction by A2, A13, AFF_1:39; :: thesis: verum

end;

hence a3,a4 // b3,b4 by A39, A40, AFF_1:11; :: thesis: verum

end;

now

assume A41: a3 = b1 ; :: thesis: a3,a4 // b3,b4
A42: LIN a1,a3,b3 by A2, AFF_1:33;
a3 <> b3

proof

assume a3 = b3 ; :: thesis: contradiction
then a3,a2 // b2,b1 by A2, A41, AFF_1:13;
then a3,a2 // a2,a1 by A2, AFF_1:14;
then a2,a3 // a2,a1 by AFF_1:13;
then LIN a2,a3,a1 by AFF_1:def 1;
then LIN a1,a3,a2 by AFF_1:15;
hence contradiction by A2, A13, AFF_1:39; :: thesis: verum

end;

then A43: a1 = b3 by A13, A31, A42;
A44: LIN a2,a4,b2 by A2, AFF_1:33;
a2 <> b2

proof

assume a2 = b2 ; :: thesis: contradiction
then LIN a2,a1,a3 by A2, A41, AFF_1:def 1;
then LIN a1,a3,a2 by AFF_1:15;
hence contradiction by A2, A13, AFF_1:39; :: thesis: verum

end;

then A45: a4 = b2 by A13, A31, A44;
A46: LIN a2,a4,b4 by A2, AFF_1:33;
a4 <> b4

proof

assume a4 = b4 ; :: thesis: contradiction
then a4,a1 // a4,a3 by A2, A41, AFF_1:13;
then LIN a4,a1,a3 by AFF_1:def 1;
then LIN a1,a3,a4 by AFF_1:15;
hence contradiction by A2, A13, AFF_1:39; :: thesis: verum

end;

then A47: a2 = b4 by A13, A31, A46;
a3,a4 // b2,b1 by A41, A45, AFF_1:11;
then a3,a4 // b4,b3 by A2, A43, A47, AFF_1:14;
hence a3,a4 // b3,b4 by AFF_1:13; :: thesis: verum

end;

hence a3,a4 // b3,b4 by A13, A31, A32, A33; :: thesis: verum

end;

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

end;

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

end;

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