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

assume A2: 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, a', b', c' be Element of AP; :: thesis:
assume ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a' & o <> b & o <> b' & o <> c & o <> c' & a in M & b in M & c in M & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' ) ; :: thesis:
hence a,c' // c,a' by A2, 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, a', b', c' be Element of AP; :: thesis:
assume ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' ) ; :: thesis:
hence a,c' // c,a' by A2, Def1; :: thesis:

end;

assume A3: ( AP is Pappian & 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, a', b', c' be Element of AP; :: thesis:
assume A4: ( M is being_line & N is being_line & a in M & b in M & c in M & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' ) ; :: thesis:

assume A5: M <> N ; :: thesis:
assume A6: not a,c' // c,a' ; :: thesis:

assume not M // N ; :: thesis:
then consider o being Element of AP such that
A7: ( o in M & o in N ) by A4, AFF_1:72;
A8: o <> a

assume A9: o = a ; :: thesis:
then o,b' // a',b by A4, AFF_1:13;
then ( o = b' or b in N ) by A4, A7, AFF_1:62;
then ( o = b' or o = b ) by A4, A5, A7, AFF_1:30;
then ( c,o // b,c' or o,c' // b',c ) by A4, AFF_1:13;
then ( c' in M or c = o or c in N or o = c' ) by A4, A7, AFF_1:62;
then ( o = c or o = c' ) by A4, A5, A7, AFF_1:30;
hence contradiction by A4, A6, A7, A9, AFF_1:12, AFF_1:65; :: thesis:

end;

A10: o <> b

assume A11: o = b ; :: thesis:
then o,a' // b',a by A4, AFF_1:13;
then A12: ( o = a' or a in N ) by A4, A7, AFF_1:62;
o,c' // b',c by A4, A11, AFF_1:13;
then ( o = c' or c in N ) by A4, A7, AFF_1:62;
then ( o = c' or o = c ) by A4, A5, A7, AFF_1:30;
hence contradiction by A4, A5, A6, A7, A8, A12, AFF_1:12, AFF_1:30, AFF_1:65; :: thesis:

end;

A13: o <> c

assume A14: o = c ; :: thesis:
then o,b' // c',b by A4, AFF_1:13;
then ( o = b' or b in N ) by A4, A7, AFF_1:62;
then a' in M by A4, A7, A8, A10, AFF_1:30, AFF_1:62;
then a' = o by A4, A5, A7, AFF_1:30;
hence contradiction by A6, A14, AFF_1:12; :: thesis:

end;

A15: o <> a'

assume A16: o = a' ; :: thesis:
then o,b // a,b' by A4, AFF_1:13;
then b' in M by A4, A7, A10, AFF_1:62;
then o = b' by A4, A5, A7, AFF_1:30;
then c,o // b,c' by A4, AFF_1:13;
then ( a' in M & c' in M ) by A4, A7, A13, A16, AFF_1:62;
hence contradiction by A4, A6, AFF_1:65; :: thesis:

end;

A17: o <> b'

assume A18: o = b' ; :: thesis:
then o,c // b,c' by A4, AFF_1:13;
then ( a' in M & c' in M ) by A4, A7, A8, A13, A18, AFF_1:62;
hence contradiction by A4, A6, AFF_1:65; :: thesis:

end;

o <> c'

assume A19: o = c' ; :: thesis:
then b' in M by A4, A7, A10, AFF_1:62;
then a,o // b,a' by A4, A5, A7, AFF_1:30;
then ( a' in M & c' in M ) by A4, A7, A8, A19, AFF_1:62;
hence contradiction by A4, A6, AFF_1:65; :: thesis:

end;

hence a,c' // c,a' by A3, A4, A5, A7, A8, A10, A13, A15, A17, Def2; :: thesis:

end;

hence a,c' // c,a' by A3, A4, A5, Def13; :: thesis:

end;

hence a,c' // c,a' by A4, AFF_1:65; :: thesis:

end;

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