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

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 A2: ( 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 ) ; :: thesis: a3,a4 // b3,b4
then A3: ( M is being_line & N is being_line ) by AFF_1:50;
then A4: ( M // M & N // N ) by 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
b1 = b3

proof

assume A9: b1 <> b3 ; :: thesis: contradiction
A10: LIN b2,b1,b3

proof

LIN a2,a1,a3 by A8, AFF_1:16;
then a2,a1 // a2,a3 by AFF_1:def 1;
then b2,b1 // a2,a3 by A2, AFF_1:14;
then b2,b1 // a3,a2 by AFF_1:13;
then b2,b1 // b3,b2 by A2, AFF_1:14;
then b2,b1 // b2,b3 by AFF_1:13;
hence LIN b2,b1,b3 by AFF_1:def 1; :: thesis: verum

end;

b1,b3 // N by A2, AFF_1:54;
hence contradiction by A2, A9, A10, AFF_1:60; :: thesis: verum

end;

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

end;

now

assume A11: a2 = a4 ; :: thesis: a3,a4 // b3,b4
A12: b2,b4 // M by A2, AFF_1:54;
LIN a1,a4,a2 by A11, AFF_1:16;
then a1,a4 // a1,a2 by AFF_1:def 1;
then b1,b4 // a1,a2 by A2, AFF_1:14;
then b1,b4 // a2,a1 by AFF_1:13;
then b1,b4 // b2,b1 by A2, AFF_1:14;
then b1,b2 // b1,b4 by AFF_1:13;
then LIN b1,b2,b4 by AFF_1:def 1;
hence a3,a4 // b3,b4 by A2, A11, A12, AFF_1:60; :: thesis: verum

end;

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

end;

now

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

A14: now

assume A15: 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
a1,a3 // a1,b1 by A2, A4, AFF_1:53;
then A16: LIN a1,a3,b1 by AFF_1:def 1;

A17: now

assume A18: a1 = b1 ; :: thesis: a3,a4 // b3,b4
then A19: LIN a1,a4,b4 by A2, AFF_1:def 1;
a4,b4 // M by A2, AFF_1:54;
then A20: a4 = b4 by A2, A19, AFF_1:60;
a1,a2 // a1,b2 by A2, A18, AFF_1:13;
then A21: LIN a1,a2,b2 by AFF_1:def 1;
a2,b2 // M by A2, AFF_1:54;
then a2 = b2 by A2, A21, AFF_1:60;
then a2,a3 // a2,b3 by A2, AFF_1:13;
then A22: LIN a2,a3,b3 by AFF_1:def 1;
a3,b3 // N by A2, AFF_1:54;
then a3 = b3 by A2, A22, AFF_1:60;
hence a3,a4 // b3,b4 by A20, AFF_1:11; :: thesis: verum

end;

now

assume A23: a3 = b1 ; :: thesis: a3,a4 // b3,b4
a2,a4 // a2,b2 by A2, A4, AFF_1:53;
then A24: LIN a2,a4,b2 by AFF_1:def 1;

A25: now

assume A26: a4 = b2 ; :: thesis: a3,a4 // b3,b4
a1,a3 // a1,b3 by A2, A4, AFF_1:53;
then A27: LIN a1,a3,b3 by AFF_1:def 1;
a3 <> b3

proof

assume a3 = b3 ; :: thesis: contradiction
then A28: LIN a3,a2,b2 by A2, AFF_1:def 1;
a2,b2 // M by A2, AFF_1:54;
hence contradiction by A2, A13, A26, A28, AFF_1:60; :: thesis: verum

end;

then A29: a1 = b3 by A13, A15, A27;
a2,a4 // a2,b4 by A2, A4, AFF_1:53;
then A30: LIN a2,a4,b4 by AFF_1:def 1;
a4 <> b4

proof

assume a4 = b4 ; :: thesis: contradiction
then a4,a1 // a4,b1 by A2, AFF_1:13;
then A31: LIN a4,a1,b1 by AFF_1:def 1;
a1,b1 // N by A2, AFF_1:54;
hence contradiction by A2, A13, A23, A31, AFF_1:60; :: thesis: verum

end;

then A32: a2 = b4 by A13, A15, A30;
a3,a4 // b2,b1 by A23, A26, AFF_1:11;
then a3,a4 // a2,a1 by A2, AFF_1:14;
hence a3,a4 // b3,b4 by A29, A32, AFF_1:13; :: thesis: verum

end;

now

assume a2 = b2 ; :: thesis: a3,a4 // b3,b4
then A33: LIN a2,a1,b1 by A2, AFF_1:def 1;
a1,b1 // N by A2, AFF_1:54;
hence a3,a4 // b3,b4 by A2, A17, A33, AFF_1:60; :: thesis: verum

end;

hence a3,a4 // b3,b4 by A13, A15, A24, A25; :: thesis: verum

end;

hence a3,a4 // b3,b4 by A13, A15, A16, A17; :: thesis: verum

end;

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
A34: ( LIN a1,a2,d & a1 <> d & a2 <> d ) by A2, TRANSLAC:2;
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
A35: ( d in Y & M // Y ) by A3, AFF_1:63;
take Y ; :: thesis: ( Y is being_line & d in Y & Y // M )
thus ( Y is being_line & d in Y & Y // M ) by A35, AFF_1:50; :: thesis: verum

end;

then consider Y being Subset of X such that
A36: ( Y is being_line & d in Y & Y // M ) ;
A37: ( Y // Y & M // M & N // N ) by A3, A36, AFF_1:55;
ex d1 being Element of X st
( d1 in Y & b1,b2 // b1,d1 )

proof

consider e1 being Element of X such that
A38: ( d <> e1 & e1 in Y ) by A36, AFF_1:32;
consider e2 being Element of X such that
A39: ( b1,b2 // b1,e2 & b1 <> e2 ) by DIRAF:47;
not d,e1 // b1,e2

proof

assume d,e1 // b1,e2 ; :: thesis: contradiction
then A40: d,e1 // b1,b2 by A39, AFF_1:14;
d,e1 // Y by A36, A37, A38, AFF_1:54;
then A41: b1,b2 // Y by A38, A40, AFF_1:46;
a1,a3 // Y by A2, A36, AFF_1:54;
then a1,a3 // b1,b2 by A36, A41, AFF_1:45;
then a1,a3 // b2,b1 by AFF_1:13;
then a1,a3 // a2,a1 by A2, 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, A3, A13, AFF_1:39; :: thesis: verum

end;

then consider d1 being Element of X such that
A42: ( LIN d,e1,d1 & LIN b1,e2,d1 ) by AFF_1:74;
take d1 ; :: thesis: ( d1 in Y & b1,b2 // b1,d1 )
b1,e2 // b1,d1 by A42, AFF_1:def 1;
hence ( d1 in Y & b1,b2 // b1,d1 ) by A36, A38, A39, A42, AFF_1:14, AFF_1:39; :: thesis: verum

end;

then consider d1 being Element of X such that
A43: ( d1 in Y & b1,b2 // b1,d1 ) ;
A44: ( N // Y & N // M ) by A2, A36, AFF_1:58;
A45: ( N <> M & N <> Y & Y <> M )

proof

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

A47: now

assume N = Y ; :: thesis: contradiction
then A48: a2,d // a2,a4 by A2, A36, A37, AFF_1:53;
LIN a2,d,a1 by A34, AFF_1:15;
then a2,d // a2,a1 by AFF_1:def 1;
then a2,a4 // a2,a1 by A34, A48, AFF_1:14;
then LIN a2,a4,a1 by AFF_1:def 1;
hence contradiction by A2, A3, A13, AFF_1:39; :: thesis: verum

end;

now

assume Y = M ; :: thesis: contradiction
then A49: a1,d // a1,a3 by A2, A36, AFF_1:53;
a1,a2 // a1,d by A34, AFF_1:def 1;
then a1,a3 // a1,a2 by A34, A49, AFF_1:14;
then LIN a1,a3,a2 by AFF_1:def 1;
hence contradiction by A2, A3, A13, AFF_1:39; :: thesis: verum

end;

hence contradiction by A2, A46, A47; :: thesis: verum

end;

LIN a2,a1,d by A34, AFF_1:15;
then a2,a1 // a2,d by AFF_1:def 1;
then A50: b2,b1 // a2,d by A2, AFF_1:14;
LIN b1,b2,d1 by A43, AFF_1:def 1;
then LIN b2,b1,d1 by AFF_1:15;
then b2,b1 // b2,d1 by AFF_1:def 1;
then ( a2,d // b2,d1 & a2,a3 // b2,b3 ) by A2, A50, AFF_1:13, AFF_1:14;
then A51: d,a3 // d1,b3 by A1, A2, A3, A36, A43, A44, A45, AFF_2:def 11;
a1,d // b1,d1

proof

a1,a2 // a1,d by A34, AFF_1:def 1;
then a2,a1 // a1,d by AFF_1:13;
then b2,b1 // a1,d by A2, AFF_1:14;
then b1,b2 // a1,d by AFF_1:13;
hence a1,d // b1,d1 by A2, A43, AFF_1:14; :: thesis: verum

end;

then A52: d,a4 // d1,b4 by A1, A2, A3, A36, A43, A45, AFF_2:def 11;
Y // N by A2, A36, AFF_1:58;
hence a3,a4 // b3,b4 by A1, A2, A3, A36, A43, A45, A51, A52, AFF_2:def 11; :: thesis: verum

end;

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

end;

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

end;

hence X is satisfying_minor_Scherungssatz by Def1; :: thesis: verum