let AP be AffinPlane; :: thesis:

A1: now

assume A2: 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, a9, b9, c9 be Element of AP; :: thesis:
assume that
A3: M is being_line and
A4: N is being_line and
A5: ( M <> N & o in M & o in N ) and
A6: o <> a and
A7: o <> a9 and
A8: o <> b and
A9: o <> b9 and
A10: ( o <> c & o <> c9 ) and
A11: a in M and
A12: b in M and
A13: c in M and
A14: a9 in N and
A15: b9 in N and
A16: c9 in N and
A17: a,b9 // b,a9 and
A18: b,c9 // c,b9 ; :: thesis:
set A = Line a,c9;
set P = Line b,a9;
A19: b <> a9 by A3, A4, A5, A7, A12, A14, AFF_1:30;
then A20: b in Line b,a9 by AFF_1:38;
assume A21: not a,c9 // c,a9 ; :: thesis:
then A22: a <> c9 by AFF_1:12;
then A23: ( a in Line a,c9 & c9 in Line a,c9 ) by AFF_1:38;
A24: a9 in Line b,a9 by A19, AFF_1:38;
Line a,c9 is being_line by A22, AFF_1:38;
then consider K being Subset of AP such that
A25: c in K and
A26: Line a,c9 // K by AFF_1:63;
A27: b <> c

proof

assume A28: b = c ; :: thesis:
then LIN b,c9,b9 by A18, AFF_1:def 1;
then LIN b9,c9,b by AFF_1:15;
then ( b9 = c9 or b in N ) by A4, A15, A16, AFF_1:39;
hence contradiction by A3, A4, A5, A8, A12, A17, A21, A28, AFF_1:30; :: thesis:

end;

A29: b9 <> c9

proof

assume b9 = c9 ; :: thesis:
then b9,b // b9,c by A18, AFF_1:13;
then LIN b9,b,c by AFF_1:def 1;
then LIN b,c,b9 by AFF_1:15;
then b9 in M by A3, A12, A13, A27, AFF_1:39;
hence contradiction by A3, A4, A5, A9, A15, AFF_1:30; :: thesis:

end;

A30: not Line b,a9 // K

proof

assume Line b,a9 // K ; :: thesis:
then Line b,a9 // Line a,c9 by A26, AFF_1:58;
then b,a9 // a,c9 by A23, A20, A24, AFF_1:53;
then a,b9 // a,c9 by A17, A19, AFF_1:14;
then LIN a,b9,c9 by AFF_1:def 1;
then LIN b9,c9,a by AFF_1:15;
then a in N by A4, A15, A16, A29, AFF_1:39;
hence contradiction by A3, A4, A5, A6, A11, AFF_1:30; :: thesis:

end;

A31: Line b,a9 is being_line by A19, AFF_1:38;
K is being_line by A26, AFF_1:50;
then consider x being Element of AP such that
A32: x in Line b,a9 and
A33: x in K by A31, A30, AFF_1:72;
A34: a,c9 // c,x by A23, A25, A26, A33, AFF_1:53;
LIN b,x,a9 by A31, A20, A24, A32, AFF_1:33;
then b,x // b,a9 by AFF_1:def 1;
then a,b9 // b,x by A17, A19, AFF_1:14;
then x in N by A2, A3, A4, A5, A6, A8, A9, A10, A11, A12, A13, A15, A16, A18, A27, A34, Def3;
then N = Line b,a9 by A4, A14, A21, A31, A24, A32, A34, AFF_1:30;
hence contradiction by A3, A4, A5, A8, A12, A20, AFF_1:30; :: thesis:

end;

end;

now

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

proof

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, a9, b9, c9 be Element of AP; :: thesis:
assume that
A36: M is being_line and
A37: N is being_line and
A38: M <> N and
A39: o in M and
A40: o in N and
A41: o <> a and
o <> a9 and
A42: o <> b and
A43: o <> b9 and
A44: o <> c and
A45: o <> c9 and
A46: a in M and
A47: b in M and
A48: c in M and
A49: b9 in N and
A50: c9 in N and
A51: a,b9 // b,a9 and
A52: b,c9 // c,b9 and
A53: a,c9 // c,a9 and
A54: b <> c ; :: thesis:
A55: a <> c9 by A36, A37, A38, A39, A40, A41, A46, A50, AFF_1:30;
A56: b <> a9

proof

assume b = a9 ; :: thesis:
then c,b // a,c9 by A53, AFF_1:13;
then c9 in M by A36, A46, A47, A48, A54, AFF_1:62;
hence contradiction by A36, A37, A38, A39, A40, A45, A50, AFF_1:30; :: thesis:

end;

not b,a9 // N

proof

assume A57: b,a9 // N ; :: thesis:
b,a9 // a,b9 by A51, AFF_1:13;
then a,b9 // N by A56, A57, AFF_1:46;
then b9,a // N by AFF_1:48;
then a in N by A37, A49, AFF_1:37;
hence contradiction by A36, A37, A38, A39, A40, A41, A46, AFF_1:30; :: thesis:

end;

then consider x being Element of AP such that
A58: x in N and
A59: LIN b,a9,x by A37, AFF_1:73;
A60: b,a9 // b,x by A59, AFF_1:def 1;
A61: o <> x

proof

assume o = x ; :: thesis:
then b,o // a,b9 by A51, A56, A60, AFF_1:14;
then b9 in M by A36, A39, A42, A46, A47, AFF_1:62;
hence contradiction by A36, A37, A38, A39, A40, A43, A49, AFF_1:30; :: thesis:

end;

a,b9 // b,x by A51, A56, A60, AFF_1:14;
then a,c9 // c,x by A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A45, A46, A47, A48, A49, A50, A52, A58, A61, Def2;
then c,a9 // c,x by A53, A55, AFF_1:14;
then LIN c,a9,x by AFF_1:def 1;
then A62: LIN a9,x,c by AFF_1:15;
A63: LIN a9,x,x by AFF_1:16;
assume A64: not a9 in N ; :: thesis:
LIN a9,x,b by A59, AFF_1:15;
then x in M by A36, A47, A48, A54, A64, A58, A62, A63, AFF_1:17, AFF_1:39;
hence contradiction by A36, A37, A38, A39, A40, A58, A61, AFF_1:30; :: thesis:

end;

end;

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