let X be AffinPlane; :: thesis: ( X is satisfying_pap iff X is satisfying_minor_indirect_Scherungssatz )
A1: ( X is satisfying_pap implies X is satisfying_minor_indirect_Scherungssatz )

proof

assume A2: X is satisfying_pap ; :: thesis: X is satisfying_minor_indirect_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 & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 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 & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 )
assume A3: ( M // N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 ) ; :: thesis: a3,a4 // b3,b4
then A4: ( M is being_line & N is being_line ) by AFF_1:50;
( a1,a2 // b2,b1 & b2,b3 // a3,a2 ) by A3, AFF_1:13;
then a1,b3 // a3,b1 by A2, A3, A4, AFF_2:def 13;
then A5: b1,a3 // b3,a1 by AFF_1:13;
a4,a1 // b1,b4 by A3, AFF_1:13;
then a4,a3 // b3,b4 by A2, A3, A4, A5, AFF_2:def 13;
hence a3,a4 // b3,b4 by AFF_1:13; :: thesis: verum

end;

hence X is satisfying_minor_indirect_Scherungssatz by Def5; :: thesis: verum

end;

( X is satisfying_minor_indirect_Scherungssatz implies X is satisfying_pap )

proof

assume A6: X is satisfying_minor_indirect_Scherungssatz ; :: thesis: X is satisfying_pap

now

let M, N be Subset of X; :: thesis: for a, b, c, a1, b1, c1 being Element of X st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 holds
a,c1 // c,a1
let a, b, c, a1, b1, c1 be Element of X; :: thesis: ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 implies a,c1 // c,a1 )
assume A7: ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 ) ; :: thesis: a,c1 // c,a1
then A8: ( not a in N & not b in N & not c in N ) by AFF_1:59;
A9: ( not a1 in M & not b1 in M & not c1 in M ) by A7, AFF_1:59;
A10: ( a,b1 // a1,b & b,c1 // b1,c ) by A7, AFF_1:13;
b1,b // b,b1 by AFF_1:11;
then a,c1 // a1,c by A6, A7, A8, A9, A10, Def5;
hence a,c1 // c,a1 by AFF_1:13; :: thesis: verum

end;

hence X is satisfying_pap by AFF_2:def 13; :: thesis: verum

end;

hence ( X is satisfying_pap iff X is satisfying_minor_indirect_Scherungssatz ) by A1; :: thesis: verum