A1: now

assume A2: AP is Pappian ; :: thesis:
thus AP is satisfying_PAP_1 :: thesis:

let M be Subset of AP; :: according to AFF_2:def 3 :: thesis:
let N be Subset of AP; :: thesis:
let o, a, b, c, a', b', c' be Element of AP; :: thesis:
assume A3: ( 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 & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' & a,c' // c,a' & b <> c ) ; :: thesis:
assume A4: not a' in N ; :: thesis:
A5: ( a <> b' & a <> c' ) by A3, AFF_1:30;
A6: b <> a'

proof

assume b = a' ; :: thesis:
then c,b // a,c' by A3, AFF_1:13;
then c' in M by A3, AFF_1:62;
hence contradiction by A3, AFF_1:30; :: thesis:

end;

not b,a' // N

proof

assume b,a' // N ; :: thesis:
then ( b,a' // N & b,a' // a,b' ) by A3, AFF_1:13;
then a,b' // N by A6, AFF_1:46;
then b',a // N by AFF_1:48;
then a in N by A3, AFF_1:37;
hence contradiction by A3, AFF_1:30; :: thesis:

end;

then consider x being Element of AP such that
A7: ( x in N & LIN b,a',x ) by A3, AFF_1:73;
A8: a,b' // b,x

proof

b,a' // b,x by A7, AFF_1:def 1;
hence a,b' // b,x by A3, A6, AFF_1:14; :: thesis:

end;

A9: o <> x

proof

assume o = x ; :: thesis:
then b,o // a,b' by A8, AFF_1:13;
then b' in M by A3, AFF_1:62;
hence contradiction by A3, AFF_1:30; :: thesis:

end;

then a,c' // c,x by A2, A3, A7, A8, Def2;
then c,a' // c,x by A3, A5, AFF_1:14;
then LIN c,a',x by AFF_1:def 1;
then ( LIN a',x,c & LIN a',x,b & LIN a',x,x ) by A7, AFF_1:15, AFF_1:16;
then LIN b,c,x by A4, A7, AFF_1:17;
then x in M by A3, AFF_1:39;
hence contradiction by A3, A7, A9, AFF_1:30; :: thesis:

end;

now

assume A10: AP is satisfying_PAP_1 ; :: thesis:
thus AP is Pappian :: thesis:

proof

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 A11: ( 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:
assume A12: not a,c' // c,a' ; :: thesis:
then A13: ( a <> c' & c <> a' ) by AFF_1:12;
A14: ( a <> b' & b <> a' ) by A11, AFF_1:30;
A15: b <> c

proof

assume A16: b = c ; :: thesis:
then LIN b,c',b' by A11, AFF_1:def 1;
then LIN b',c',b by AFF_1:15;
then ( b' = c' or b in N ) by A11, AFF_1:39;
hence contradiction by A11, A12, A16, AFF_1:30; :: thesis:

end;

A17: b' <> c'

proof

assume b' = c' ; :: thesis:
then b',b // b',c by A11, AFF_1:13;
then LIN b',b,c by AFF_1:def 1;
then LIN b,c,b' by AFF_1:15;
then b' in M by A11, A15, AFF_1:39;
hence contradiction by A11, AFF_1:30; :: thesis:

end;

set A = Line a,c';
set P = Line b,a';
A18: ( Line a,c' is being_line & Line b,a' is being_line & a in Line a,c' & c' in Line a,c' & b in Line b,a' & a' in Line b,a' ) by A13, A14, AFF_1:38;
then consider K being Subset of AP such that
A19: ( c in K & Line a,c' // K ) by AFF_1:63;
A20: ( K is being_line & K // Line a,c' ) by A19, AFF_1:50;
not Line b,a' // K

proof

assume Line b,a' // K ; :: thesis:
then Line b,a' // Line a,c' by A19, AFF_1:58;
then b,a' // a,c' by A18, AFF_1:53;
then a,b' // a,c' by A11, A14, AFF_1:14;
then LIN a,b',c' by AFF_1:def 1;
then LIN b',c',a by AFF_1:15;
then a in N by A11, A17, AFF_1:39;
hence contradiction by A11, AFF_1:30; :: thesis:

end;

then consider x being Element of AP such that
A21: ( x in Line b,a' & x in K ) by A18, A20, AFF_1:72;
A22: a,c' // c,x by A18, A19, A21, AFF_1:53;
a,b' // b,x

proof

LIN b,x,a' by A18, A21, AFF_1:33;
then b,x // b,a' by AFF_1:def 1;
hence a,b' // b,x by A11, A14, AFF_1:14; :: thesis:

end;

then x in N by A10, A11, A15, A22, Def3;
then N = Line b,a' by A11, A12, A18, A21, A22, AFF_1:30;
hence contradiction by A11, A18, AFF_1:30; :: thesis:

end;

hence ( AP is Pappian iff AP is satisfying_PAP_1 ) by A1; :: thesis: