let AP be AffinPlane; :: thesis:
A1: ( AP is Pappian & AP is satisfying_pap implies AP is satisfying_PPAP )

assume that
A2: AP is Pappian and
A3: AP is satisfying_pap ; :: thesis:
thus AP is satisfying_PPAP :: thesis:

let M be Subset of AP; :: according to AFF_2:def 1 :: thesis:
let N be Subset of AP; :: thesis:
let a, b, c, a9, b9, c9 be Element of AP; :: thesis:
assume that
A4: M is being_line and
A5: N is being_line and
A6: a in M and
A7: b in M and
A8: c in M and
A9: a9 in N and
A10: b9 in N and
A11: c9 in N and
A12: a,b9 // b,a9 and
A13: b,c9 // c,b9 ; :: thesis:

assume A14: M <> N ; :: thesis:
assume A15: not a,c9 // c,a9 ; :: thesis:

assume not M // N ; :: thesis:
then consider o being Element of AP such that
A16: o in M and
A17: o in N by A4, A5, AFF_1:72;
A18: o <> a

assume A19: o = a ; :: thesis:
then o,b9 // a9,b by A12, AFF_1:13;
then ( o = b9 or b in N ) by A5, A9, A10, A17, AFF_1:62;
then ( o = b9 or o = b ) by A4, A5, A7, A14, A16, A17, AFF_1:30;
then ( c,o // b,c9 or o,c9 // b9,c ) by A13, AFF_1:13;
then ( c9 in M or c = o or c in N or o = c9 ) by A4, A5, A7, A8, A10, A11, A16, A17, AFF_1:62;
then ( o = c or o = c9 ) by A4, A5, A8, A11, A14, A16, A17, AFF_1:30;
hence contradiction by A5, A9, A11, A15, A17, A19, AFF_1:12, AFF_1:65; :: thesis:

end;

assume A21: o = b ; :: thesis:
then o,c9 // b9,c by A13, AFF_1:13;
then ( o = c9 or c in N ) by A5, A10, A11, A17, AFF_1:62;
then A22: ( o = c9 or o = c ) by A4, A5, A8, A14, A16, A17, AFF_1:30;
o,a9 // b9,a by A12, A21, AFF_1:13;
then ( o = a9 or a in N ) by A5, A9, A10, A17, AFF_1:62;
hence contradiction by A4, A5, A6, A8, A14, A15, A16, A17, A18, A22, AFF_1:12, AFF_1:30, AFF_1:65; :: thesis:

end;

assume A24: o = c9 ; :: thesis:
then b9 in M by A4, A7, A8, A13, A16, A20, AFF_1:62;
then a,o // b,a9 by A4, A5, A10, A12, A14, A16, A17, AFF_1:30;
then a9 in M by A4, A6, A7, A16, A18, AFF_1:62;
hence contradiction by A4, A6, A8, A15, A16, A24, AFF_1:65; :: thesis:

end;

assume A26: o = c ; :: thesis:
then o,b9 // c9,b by A13, AFF_1:13;
then ( o = b9 or b in N ) by A5, A10, A11, A17, AFF_1:62;
then a9 in M by A4, A5, A6, A7, A9, A12, A16, A17, A18, A20, AFF_1:30, AFF_1:62;
then a9 = o by A4, A5, A9, A14, A16, A17, AFF_1:30;
hence contradiction by A15, A26, AFF_1:12; :: thesis:

end;

assume A28: o = a9 ; :: thesis:
then o,b // a,b9 by A12, AFF_1:13;
then b9 in M by A4, A6, A7, A16, A20, AFF_1:62;
then o = b9 by A4, A5, A10, A14, A16, A17, AFF_1:30;
then c,o // b,c9 by A13, AFF_1:13;
then c9 in M by A4, A7, A8, A16, A25, AFF_1:62;
hence contradiction by A4, A6, A8, A15, A16, A28, AFF_1:65; :: thesis:

end;

o <> b9

assume A29: o = b9 ; :: thesis:
then o,c // b,c9 by A13, AFF_1:13;
then A30: c9 in M by A4, A7, A8, A16, A25, AFF_1:62;
a9 in M by A4, A6, A7, A12, A16, A18, A29, AFF_1:62;
hence contradiction by A4, A6, A8, A15, A30, AFF_1:65; :: thesis:

end;

hence a,c9 // c,a9 by A2, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A16, A17, A18, A20, A25, A27, A23, Def2; :: thesis:

end;

hence a,c9 // c,a9 by A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, Def13; :: thesis:

end;

hence a,c9 // c,a9 by A4, A6, A8, A9, A11, AFF_1:65; :: thesis:

end;

end;

( AP is satisfying_PPAP implies ( AP is Pappian & AP is satisfying_pap ) )

assume A31: AP is satisfying_PPAP ; :: thesis:
thus AP is Pappian :: thesis:

let M be Subset of AP; :: according to AFF_2:def 2 :: thesis:
let N be Subset of AP; :: thesis:
let o, a, b, c, a9, b9, c9 be Element of AP; :: thesis:
assume that
A32: ( M is being_line & N is being_line ) and
( M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 ) and
A33: ( a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 ) ; :: thesis:
thus a,c9 // c,a9 by A31, A32, A33, Def1; :: thesis:

end;

thus AP is satisfying_pap :: thesis:

let M be Subset of AP; :: according to AFF_2:def 13 :: thesis:
let N be Subset of AP; :: thesis:
let a, b, c, a9, b9, c9 be Element of AP; :: thesis:
assume that
A34: ( M is being_line & N is being_line & a in M & b in M & c in M ) and
( M // N & M <> N ) and
A35: ( a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 ) ; :: thesis:
thus a,c9 // c,a9 by A31, A34, A35, Def1; :: thesis:

end;

end;

hence ( AP is satisfying_PPAP iff ( AP is Pappian & AP is satisfying_pap ) ) by A1; :: thesis: