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