let AP be AffinPlane; :: thesis: ( AP is Pappian implies AP is satisfying_pap )
assume A1: AP is Pappian ; :: thesis: AP is satisfying_pap
thus AP is satisfying_pap :: thesis: verum

proof

let M be Subset of AP; :: according to AFF_2:def 13 :: thesis: for N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let N be Subset of AP; :: thesis: for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )
assume that
A2: M is being_line and
A3: N is being_line and
A4: a in M and
A5: b in M and
A6: c in M and
A7: M // N and
A8: M <> N 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: a,c9 // c,a9
A14: b <> a9 by A5, A7, A8, A9, AFF_1:59;
set K = Line a,c9;
set C = Line c,b9;
A15: c <> b9 by A6, A7, A8, A10, AFF_1:59;
then A16: Line c,b9 is being_line by AFF_1:38;
assume A17: not a,c9 // c,a9 ; :: thesis: contradiction

A18: now

assume A19: a = b ; :: thesis: contradiction
then LIN a,b9,a9 by A12, AFF_1:def 1;
then LIN a9,b9,a by AFF_1:15;
then ( a9 = b9 or a in N ) by A3, A9, A10, AFF_1:39;
hence contradiction by A4, A7, A8, A13, A17, A19, AFF_1:59; :: thesis: verum

end;

A20: now

assume a9 = b9 ; :: thesis: contradiction
then a9,a // a9,b by A12, AFF_1:13;
then LIN a9,a,b by AFF_1:def 1;
then LIN a,b,a9 by AFF_1:15;
then a9 in M by A2, A4, A5, A18, AFF_1:39;
hence contradiction by A7, A8, A9, AFF_1:59; :: thesis: verum

end;

A21: now

assume A22: b = c ; :: thesis: contradiction
then LIN b,c9,b9 by A13, AFF_1:def 1;
then LIN b9,c9,b by AFF_1:15;
then ( b9 = c9 or b in N ) by A3, A10, A11, AFF_1:39;
hence contradiction by A5, A7, A8, A12, A17, A22, AFF_1:59; :: thesis: verum

end;

A23: now

assume b9 = c9 ; :: thesis: contradiction
then b9,b // b9,c by A13, 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 A2, A5, A6, A21, AFF_1:39;
hence contradiction by A7, A8, A10, AFF_1:59; :: thesis: verum

end;

A24: a <> c9 by A4, A7, A8, A11, AFF_1:59;
then A25: a in Line a,c9 by AFF_1:38;
Line a,c9 is being_line by A24, AFF_1:38;
then consider T being Subset of AP such that
A26: a9 in T and
A27: Line a,c9 // T by AFF_1:63;
A28: T is being_line by A27, AFF_1:50;
A29: c9 in Line a,c9 by A24, AFF_1:38;
A30: ( c in Line c,b9 & b9 in Line c,b9 ) by A15, AFF_1:38;
not Line c,b9 // T

proof

assume Line c,b9 // T ; :: thesis: contradiction
then Line c,b9 // Line a,c9 by A27, AFF_1:58;
then c,b9 // a,c9 by A25, A29, A30, AFF_1:53;
then b,c9 // a,c9 by A13, A15, AFF_1:14;
then c9,b // c9,a by AFF_1:13;
then LIN c9,b,a by AFF_1:def 1;
then LIN a,b,c9 by AFF_1:15;
then c9 in M by A2, A4, A5, A18, AFF_1:39;
hence contradiction by A7, A8, A11, AFF_1:59; :: thesis: verum

end;

then consider x being Element of AP such that
A31: x in Line c,b9 and
A32: x in T by A16, A28, AFF_1:72;
set D = Line x,b;
A33: x <> b

proof

assume x = b ; :: thesis: contradiction
then LIN b,c,b9 by A16, A30, A31, AFF_1:33;
then b9 in M by A2, A5, A6, A21, AFF_1:39;
hence contradiction by A7, A8, A10, AFF_1:59; :: thesis: verum

end;

then A34: b in Line x,b by AFF_1:38;
then A35: Line x,b <> N by A5, A7, A8, AFF_1:59;
A36: Line x,b is being_line by A33, AFF_1:38;
A37: x in Line x,b by A33, AFF_1:38;
not Line x,b // N

proof

assume Line x,b // N ; :: thesis: contradiction
then Line x,b // M by A7, AFF_1:58;
then x in M by A5, A37, A34, AFF_1:59;
then ( c in T or b9 in M ) by A2, A6, A16, A30, A31, A32, AFF_1:30;
hence contradiction by A7, A8, A10, A17, A25, A29, A26, A27, AFF_1:53, AFF_1:59; :: thesis: verum

end;

then consider o being Element of AP such that
A38: o in Line x,b and
A39: o in N by A3, A36, AFF_1:72;
LIN b9,c,x by A16, A30, A31, AFF_1:33;
then A40: b9,c // b9,x by AFF_1:def 1;
A41: a9 <> x

proof

assume a9 = x ; :: thesis: contradiction
then b9,a9 // b9,c by A40, AFF_1:13;
then LIN b9,a9,c by AFF_1:def 1;
then c in N by A3, A9, A10, A20, AFF_1:39;
hence contradiction by A6, A7, A8, AFF_1:59; :: thesis: verum

end;

A42: now

assume o = x ; :: thesis: contradiction
then N = T by A3, A9, A26, A28, A32, A39, A41, AFF_1:30;
then N = Line a,c9 by A11, A29, A27, AFF_1:59;
hence contradiction by A4, A7, A8, A25, AFF_1:59; :: thesis: verum

end;

A43: a,c9 // x,a9 by A25, A29, A26, A27, A32, AFF_1:53;

A44: now

assume o = a9 ; :: thesis: contradiction
then LIN a9,b,x by A36, A37, A34, A38, AFF_1:33;
then a9,b // a9,x by AFF_1:def 1;
then b,a9 // x,a9 by AFF_1:13;
then a,b9 // x,a9 by A12, A14, AFF_1:14;
then a,b9 // a,c9 by A43, A41, 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 A3, A10, A11, A23, AFF_1:39;
hence contradiction by A4, A7, A8, AFF_1:59; :: thesis: verum

end;

c,b9 // x,b9 by A40, AFF_1:13;
then A45: b,c9 // x,b9 by A13, A15, AFF_1:14;
A46: a <> b9 by A4, A7, A8, A10, AFF_1:59;
not a,b9 // Line x,b

proof

assume a,b9 // Line x,b ; :: thesis: contradiction
then b,a9 // Line x,b by A12, A46, AFF_1:46;
then a9 in Line x,b by A36, A34, AFF_1:37;
then b in T by A26, A28, A32, A36, A37, A34, A41, AFF_1:30;
then b,a9 // a,c9 by A25, A29, A26, A27, AFF_1:53;
then a,b9 // a,c9 by A12, A14, 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 A3, A10, A11, A23, AFF_1:39;
hence contradiction by A4, A7, A8, AFF_1:59; :: thesis: verum

end;

then consider y being Element of AP such that
A47: y in Line x,b and
A48: LIN a,b9,y by A36, AFF_1:73;
A49: LIN a,y,a by AFF_1:16;
A50: b9 <> x

proof

assume b9 = x ; :: thesis: contradiction
then a,c9 // a9,b9 by A25, A29, A26, A27, A32, AFF_1:53;
then a,c9 // N by A3, A9, A10, A20, AFF_1:41;
then c9,a // N by AFF_1:48;
then a in N by A3, A11, AFF_1:37;
hence contradiction by A4, A7, A8, AFF_1:59; :: thesis: verum

end;

A51: now

assume o = b9 ; :: thesis: contradiction
then LIN b9,x,b by A36, A37, A34, A38, AFF_1:33;
then b9,x // b9,b by AFF_1:def 1;
then x,b9 // b,b9 by AFF_1:13;
then b,c9 // b,b9 by A45, A50, AFF_1:14;
then LIN b,c9,b9 by AFF_1:def 1;
then LIN b9,c9,b by AFF_1:15;
then b in N by A3, A10, A11, A23, AFF_1:39;
hence contradiction by A5, A7, A8, AFF_1:59; :: thesis: verum

end;

A52: now

assume o = y ; :: thesis: contradiction
then LIN b9,o,a by A48, AFF_1:15;
then a in N by A3, A10, A39, A51, AFF_1:39;
hence contradiction by A4, A7, A8, AFF_1:59; :: thesis: verum

end;

A53: b <> c9 by A5, A7, A8, A11, AFF_1:59;

A54: now

assume o = c9 ; :: thesis: contradiction
then Line x,b // Line c,b9 by A13, A15, A53, A16, A30, A36, A34, A38, AFF_1:52;
then b in Line c,b9 by A31, A37, A34, AFF_1:59;
then LIN c,b,b9 by A16, A30, AFF_1:33;
then b9 in M by A2, A5, A6, A21, AFF_1:39;
hence contradiction by A7, A8, A10, AFF_1:59; :: thesis: verum

end;

LIN b9,a,y by A48, AFF_1:15;
then b9,a // b9,y by AFF_1:def 1;
then a,b9 // y,b9 by AFF_1:13;
then A55: y,b9 // b,a9 by A12, A46, AFF_1:14;
o <> b by A5, A7, A8, A39, AFF_1:59;
then y,c9 // x,a9 by A1, A3, A9, A10, A11, A36, A37, A34, A38, A39, A45, A47, A55, A35, A51, A44, A54, A42, A52, Def2;
then y,c9 // a,c9 by A43, A41, AFF_1:14;
then c9,y // c9,a by AFF_1:13;
then LIN c9,y,a by AFF_1:def 1;
then A56: LIN a,y,c9 by AFF_1:15;
LIN a,y,b9 by A48, AFF_1:15;
then ( a in Line x,b or a in N ) by A3, A10, A11, A23, A47, A56, A49, AFF_1:17, AFF_1:39;
then Line x,b // N by A2, A4, A5, A7, A8, A18, A36, A34, AFF_1:30, AFF_1:59;
hence contradiction by A38, A39, A35, AFF_1:59; :: thesis: verum

end;