let X be AffinPlane; :: thesis:
assume A1: X is satisfying_minor_indirect_Scherungssatz ; :: thesis:

now

let a1, a2, a3, a4, b1, b2, b3, b4 be Element of X; :: thesis:
let M, N be Subset of X; :: thesis:
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:
then A3: ( M is being_line & N is being_line ) by AFF_1:50;
then consider d1 being Element of X such that
A4: ( a2 <> d1 & d1 in N ) by AFF_1:32;
ex d2 being Element of X st
( d2 in M & a2,a1 // d2,d1 )

proof

consider e1 being Element of X such that
A5: ( a1 <> e1 & e1 in M ) by A3, AFF_1:32;
consider e2 being Element of X such that
A6: ( a2,a1 // d1,e2 & d1 <> e2 ) by DIRAF:47;
not a1,e1 // d1,e2

proof

assume a1,e1 // d1,e2 ; :: thesis:
then a1,e1 // a2,a1 by A6, AFF_1:14;
then a1,e1 // a1,a2 by AFF_1:13;
then LIN a1,e1,a2 by AFF_1:def 1;
hence contradiction by A2, A3, A5, AFF_1:39; :: thesis:

end;

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

end;

then consider d2 being Element of X such that
A8: ( 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
A9: ( a2 <> e1 & e1 in N ) by A3, AFF_1:32;
consider e2 being Element of X such that
A10: ( a3,a2 // d2,e2 & d2 <> e2 ) by DIRAF:47;
not a2,e1 // d2,e2

proof

assume a2,e1 // d2,e2 ; :: thesis:
then a2,e1 // a3,a2 by A10, AFF_1:14;
then a2,e1 // a2,a3 by AFF_1:13;
then LIN a2,e1,a3 by AFF_1:def 1;
hence contradiction by A2, A3, A9, AFF_1:39; :: thesis:

end;

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

end;

then consider d3 being Element of X such that
A12: ( 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
A13: ( a1 <> e1 & e1 in M ) by A3, AFF_1:32;
consider e2 being Element of X such that
A14: ( a1,a4 // d1,e2 & d1 <> e2 ) by DIRAF:47;
not a1,e1 // d1,e2

proof

assume a1,e1 // d1,e2 ; :: thesis:
then a1,e1 // a1,a4 by A14, AFF_1:14;
then LIN a1,e1,a4 by AFF_1:def 1;
hence contradiction by A2, A3, A13, AFF_1:39; :: thesis:

end;

then consider d4 being Element of X such that
A15: ( LIN a1,e1,d4 & LIN d1,e2,d4 ) by AFF_1:74;
take d4 ; :: thesis:
d1,e2 // d1,d4 by A15, AFF_1:def 1;
hence ( d4 in M & a1,a4 // d1,d4 ) by A2, A3, A13, A14, A15, AFF_1:14, AFF_1:39; :: thesis:

end;

then consider d4 being Element of X such that
A16: ( d4 in M & a1,a4 // d1,d4 ) ;
A17: ( not d1 in M & not d3 in M & not d2 in N & not d4 in N ) by A2, A4, A8, A12, A16, AFF_1:59;
then A18: a3,a4 // d3,d4 by A1, A2, A4, A8, A12, A16, Def5;
A19: b2,b1 // d2,d1 by A2, A8, AFF_1:14;
A20: b3,b2 // d3,d2 by A2, A12, AFF_1:14;
b1,b4 // d1,d4 by A2, A16, AFF_1:14;
then b3,b4 // d3,d4 by A1, A2, A4, A8, A12, A16, A17, A19, A20, Def5;
hence a3,a4 // b3,b4 by A16, A17, A18, AFF_1:14; :: thesis:

end;

hence X is satisfying_minor_Scherungssatz by Def1; :: thesis: