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 :: thesis: for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
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 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 that
A2: M // N and
A3: a1 in M and
A4: a3 in M and
A5: b1 in M and
A6: b3 in M and
A7: a2 in N and
A8: a4 in N and
A9: b2 in N and
A10: b4 in N and
A11: not a4 in M and
A12: not a2 in M and
A13: not b2 in M and
not b4 in M and
A14: not a1 in N and
A15: not a3 in N and
A16: not b1 in N and
not b3 in N and
A17: a3,a2 // b3,b2 and
A18: a2,a1 // b2,b1 and
A19: a1,a4 // b1,b4 ; :: thesis: a3,a4 // b3,b4
A20: M is being_line by A2, AFF_1:36;
A21: N is being_line by A2, AFF_1:36;

A22: now :: thesis: ( a1 <> a3 & a2 <> a4 implies a3,a4 // b3,b4 )

assume that
A23: a1 <> a3 and
A24: a2 <> a4 ; :: thesis: a3,a4 // b3,b4

A25: 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
A26: LIN a1,a2,d and
A27: a1 <> d and
A28: a2 <> d by TRANSLAC:1;
A29: 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
A30: d in Y and
A31: M // Y by A20, AFF_1:49;
take Y ; :: thesis: ( Y is being_line & d in Y & Y // M )
thus ( Y is being_line & d in Y & Y // M ) by A30, A31, AFF_1:36; :: thesis: verum

end;

LIN a2,a1,d by A26, AFF_1:6;
then a2,a1 // a2,d by AFF_1:def 1;
then A32: b2,b1 // a2,d by A3, A12, A18, AFF_1:5;
A33: a2,a3 // b2,b3 by A17, AFF_1:4;
consider Y being Subset of X such that
A34: Y is being_line and
A35: d in Y and
A36: Y // M by A29;
A37: Y // N by A2, A36, AFF_1:44;
A38: ( N <> M & N <> Y & Y <> M )

proof

A39: now :: thesis: not N = Y

LIN a2,d,a1 by A26, AFF_1:6;
then A40: a2,d // a2,a1 by AFF_1:def 1;
assume N = Y ; :: thesis: contradiction
then a2,d // a2,a4 by A7, A8, A34, A35, AFF_1:39, AFF_1:41;
then a2,a4 // a2,a1 by A28, A40, AFF_1:5;
then LIN a2,a4,a1 by AFF_1:def 1;
hence contradiction by A7, A8, A14, A21, A24, AFF_1:25; :: thesis: verum

end;

A41: now :: thesis: not Y = M

assume Y = M ; :: thesis: contradiction
then A42: a1,d // a1,a3 by A3, A4, A35, A36, AFF_1:39;
a1,a2 // a1,d by A26, AFF_1:def 1;
then a1,a3 // a1,a2 by A27, A42, AFF_1:5;
then LIN a1,a3,a2 by AFF_1:def 1;
hence contradiction by A3, A4, A12, A20, A23, AFF_1:25; :: thesis: verum

end;

assume ( not N <> M or not N <> Y or not Y <> M ) ; :: thesis: contradiction
hence contradiction by A8, A11, A39, A41; :: thesis: verum

end;

A43: Y // Y by A34, AFF_1:41;
ex d1 being Element of X st
( d1 in Y & b1,b2 // b1,d1 )

proof

consider e1 being Element of X such that
A44: d <> e1 and
A45: e1 in Y by A34, AFF_1:20;
consider e2 being Element of X such that
A46: b1,b2 // b1,e2 and
A47: b1 <> e2 by DIRAF:40;
not d,e1 // b1,e2

proof

assume d,e1 // b1,e2 ; :: thesis: contradiction
then d,e1 // b1,b2 by A46, A47, AFF_1:5;
then A48: b1,b2 // Y by A35, A43, A44, A45, AFF_1:32, AFF_1:40;
a1,a3 // Y by A3, A4, A36, AFF_1:40;
then a1,a3 // b1,b2 by A34, A48, AFF_1:31;
then a1,a3 // b2,b1 by AFF_1:4;
then a1,a3 // a2,a1 by A5, A13, A18, 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 A3, A4, A12, A20, A23, AFF_1:25; :: thesis: verum

end;

then consider d1 being Element of X such that
A49: LIN d,e1,d1 and
A50: LIN b1,e2,d1 by AFF_1:60;
take d1 ; :: thesis: ( d1 in Y & b1,b2 // b1,d1 )
b1,e2 // b1,d1 by A50, AFF_1:def 1;
hence ( d1 in Y & b1,b2 // b1,d1 ) by A34, A35, A44, A45, A46, A47, A49, AFF_1:5, AFF_1:25; :: thesis: verum

end;

then consider d1 being Element of X such that
A51: d1 in Y and
A52: b1,b2 // b1,d1 ;
a1,a2 // a1,d by A26, AFF_1:def 1;
then a2,a1 // a1,d by AFF_1:4;
then b2,b1 // a1,d by A3, A12, A18, AFF_1:5;
then b1,b2 // a1,d by AFF_1:4;
then a1,d // b1,d1 by A5, A13, A52, AFF_1:5;
then A53: d,a4 // d1,b4 by A1, A2, A3, A5, A8, A10, A19, A20, A21, A34, A35, A36, A51, A38, AFF_2:def 11;
LIN b1,b2,d1 by A52, AFF_1:def 1;
then LIN b2,b1,d1 by AFF_1:6;
then b2,b1 // b2,d1 by AFF_1:def 1;
then A54: a2,d // b2,d1 by A5, A13, A32, AFF_1:5;
N // Y by A2, A36, AFF_1:44;
then d,a3 // d1,b3 by A1, A2, A4, A6, A7, A9, A20, A21, A34, A35, A51, A38, A54, A33, AFF_2:def 11;
hence a3,a4 // b3,b4 by A1, A4, A6, A8, A10, A20, A21, A34, A35, A36, A51, A38, A53, A37, AFF_2:def 11; :: thesis: verum

end;

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 A55: 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

A56: now :: thesis: ( a1 = b1 implies a3,a4 // b3,b4 )

assume A57: a1 = b1 ; :: thesis: a3,a4 // b3,b4
then A58: LIN a1,a4,b4 by A19, AFF_1:def 1;
a1,a2 // a1,b2 by A18, A57, AFF_1:4;
then A59: LIN a1,a2,b2 by AFF_1:def 1;
a2,b2 // M by A2, A7, A9, AFF_1:40;
then a2 = b2 by A3, A12, A59, AFF_1:46;
then a2,a3 // a2,b3 by A17, AFF_1:4;
then A60: LIN a2,a3,b3 by AFF_1:def 1;
a3,b3 // N by A2, A4, A6, AFF_1:40;
then A61: a3 = b3 by A7, A15, A60, AFF_1:46;
a4,b4 // M by A2, A8, A10, AFF_1:40;
then a4 = b4 by A3, A11, A58, AFF_1:46;
hence a3,a4 // b3,b4 by A61, AFF_1:2; :: thesis: verum

end;

A62: now :: thesis: ( a3 = b1 implies a3,a4 // b3,b4 )

assume A63: a3 = b1 ; :: thesis: a3,a4 // b3,b4

A64: now :: thesis: ( a4 = b2 implies a3,a4 // b3,b4 )

A65: a4 <> b4

proof

assume a4 = b4 ; :: thesis: contradiction
then a4,a1 // a4,b1 by A19, AFF_1:4;
then A66: LIN a4,a1,b1 by AFF_1:def 1;
a1,b1 // N by A2, A3, A5, AFF_1:40;
hence contradiction by A8, A14, A23, A63, A66, AFF_1:46; :: thesis: verum

end;

a2,a4 // a2,b4 by A7, A8, A10, A21, AFF_1:39, AFF_1:41;
then LIN a2,a4,b4 by AFF_1:def 1;
then A67: a2 = b4 by A24, A55, A65;
assume A68: a4 = b2 ; :: thesis: a3,a4 // b3,b4
A69: a3 <> b3

proof

assume a3 = b3 ; :: thesis: contradiction
then A70: LIN a3,a2,b2 by A17, AFF_1:def 1;
a2,b2 // M by A2, A7, A9, AFF_1:40;
hence contradiction by A4, A12, A24, A68, A70, AFF_1:46; :: thesis: verum

end;

a1,a3 // a1,b3 by A3, A4, A6, A20, AFF_1:39, AFF_1:41;
then LIN a1,a3,b3 by AFF_1:def 1;
then A71: a1 = b3 by A23, A55, A69;
a3,a4 // b2,b1 by A63, A68, AFF_1:2;
then a3,a4 // a2,a1 by A5, A13, A18, AFF_1:5;
hence a3,a4 // b3,b4 by A71, A67, AFF_1:4; :: thesis: verum

end;

A72: now :: thesis: ( a2 = b2 implies a3,a4 // b3,b4 )

assume a2 = b2 ; :: thesis: a3,a4 // b3,b4
then A73: LIN a2,a1,b1 by A18, AFF_1:def 1;
a1,b1 // N by A2, A3, A5, AFF_1:40;
hence a3,a4 // b3,b4 by A7, A14, A56, A73, AFF_1:46; :: thesis: verum

end;

a2,a4 // a2,b2 by A7, A8, A9, A21, AFF_1:39, AFF_1:41;
then LIN a2,a4,b2 by AFF_1:def 1;
hence a3,a4 // b3,b4 by A24, A55, A64, A72; :: thesis: verum

end;

a1,a3 // a1,b1 by A3, A4, A5, A20, AFF_1:39, AFF_1:41;
then LIN a1,a3,b1 by AFF_1:def 1;
hence a3,a4 // b3,b4 by A23, A55, A56, A62; :: thesis: verum

end;

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

end;

now :: thesis: ( ( a1 = a3 or a2 = a4 ) implies a3,a4 // b3,b4 )

A74: now :: thesis: ( a1 = a3 implies a3,a4 // b3,b4 )

assume A75: a1 = a3 ; :: thesis: a3,a4 // b3,b4
b1 = b3

proof

LIN a2,a1,a3 by A75, AFF_1:7;
then a2,a1 // a2,a3 by AFF_1:def 1;
then b2,b1 // a2,a3 by A3, A12, A18, AFF_1:5;
then b2,b1 // a3,a2 by AFF_1:4;
then b2,b1 // b3,b2 by A4, A12, A17, AFF_1:5;
then b2,b1 // b2,b3 by AFF_1:4;
then A76: LIN b2,b1,b3 by AFF_1:def 1;
assume A77: b1 <> b3 ; :: thesis: contradiction
b1,b3 // N by A2, A5, A6, AFF_1:40;
hence contradiction by A9, A16, A77, A76, AFF_1:46; :: thesis: verum

end;

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

end;

A78: now :: thesis: ( a2 = a4 implies a3,a4 // b3,b4 )

assume A79: a2 = a4 ; :: thesis: a3,a4 // b3,b4
then LIN a1,a4,a2 by AFF_1:7;
then a1,a4 // a1,a2 by AFF_1:def 1;
then b1,b4 // a1,a2 by A3, A11, A19, AFF_1:5;
then b1,b4 // a2,a1 by AFF_1:4;
then b1,b4 // b2,b1 by A3, A12, A18, AFF_1:5;
then b1,b2 // b1,b4 by AFF_1:4;
then A80: LIN b1,b2,b4 by AFF_1:def 1;
b2,b4 // M by A2, A9, A10, AFF_1:40;
hence a3,a4 // b3,b4 by A5, A13, A17, A79, A80, AFF_1:46; :: thesis: verum

end;

assume ( a1 = a3 or a2 = a4 ) ; :: thesis: a3,a4 // b3,b4
hence a3,a4 // b3,b4 by A74, A78; :: thesis: verum

end;

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

end;

hence X is satisfying_minor_Scherungssatz ; :: thesis: verum