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

A18: now

assume A19: a = b ; :: thesis: contradiction
then LIN a,b',a' by A12, AFF_1:def 1;
then LIN a',b',a by AFF_1:15;
then ( a' = b' 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 a' = b' ; :: thesis: contradiction
then a',a // a',b by A12, AFF_1:13;
then LIN a',a,b by AFF_1:def 1;
then LIN a,b,a' by AFF_1:15;
then a' 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,c',b' by A13, AFF_1:def 1;
then LIN b',c',b by AFF_1:15;
then ( b' = c' 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 b' = c' ; :: thesis: contradiction
then b',b // b',c by A13, 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 A2, A5, A6, A21, AFF_1:39;
hence contradiction by A7, A8, A10, AFF_1:59; :: thesis: verum

end;

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

proof

assume Line c,b' // T ; :: thesis: contradiction
then Line c,b' // Line a,c' by A27, AFF_1:58;
then c,b' // a,c' by A25, A29, A30, AFF_1:53;
then b,c' // a,c' by A13, A15, AFF_1:14;
then c',b // c',a by AFF_1:13;
then LIN c',b,a by AFF_1:def 1;
then LIN a,b,c' by AFF_1:15;
then c' 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 such that
A31: x in Line c,b' 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,b' by A16, A30, A31, AFF_1:33;
then b' 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 b' 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 such that
A38: o in Line x,b and
A39: o in N by A3, A36, AFF_1:72;
LIN b',c,x by A16, A30, A31, AFF_1:33;
then A40: b',c // b',x by AFF_1:def 1;
A41: a' <> x

proof

assume a' = x ; :: thesis: contradiction
then b',a' // b',c by A40, AFF_1:13;
then LIN b',a',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,c' by A11, A29, A27, AFF_1:59;
hence contradiction by A4, A7, A8, A25, AFF_1:59; :: thesis: verum

end;

A43: a,c' // x,a' by A25, A29, A26, A27, A32, AFF_1:53;

A44: now

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

end;

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

proof

assume a,b' // Line x,b ; :: thesis: contradiction
then b,a' // Line x,b by A12, A46, AFF_1:46;
then a' 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,a' // a,c' by A25, A29, A26, A27, AFF_1:53;
then a,b' // a,c' by A12, 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 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 such that
A47: y in Line x,b and
A48: LIN a,b',y by A36, AFF_1:73;
A49: LIN a,y,a by AFF_1:16;
A50: b' <> x

proof

assume b' = x ; :: thesis: contradiction
then a,c' // a',b' by A25, A29, A26, A27, A32, AFF_1:53;
then a,c' // N by A3, A9, A10, A20, AFF_1:41;
then c',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 = b' ; :: thesis: contradiction
then LIN b',x,b by A36, A37, A34, A38, AFF_1:33;
then b',x // b',b by AFF_1:def 1;
then x,b' // b,b' by AFF_1:13;
then b,c' // b,b' by A45, A50, AFF_1:14;
then LIN b,c',b' by AFF_1:def 1;
then LIN b',c',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 b',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 <> c' by A5, A7, A8, A11, AFF_1:59;

A54: now

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

end;

LIN b',a,y by A48, AFF_1:15;
then b',a // b',y by AFF_1:def 1;
then a,b' // y,b' by AFF_1:13;
then A55: y,b' // b,a' by A12, A46, AFF_1:14;
o <> b by A5, A7, A8, A39, AFF_1:59;
then y,c' // x,a' by A1, A3, A9, A10, A11, A36, A37, A34, A38, A39, A45, A47, A55, A35, A51, A44, A54, A42, A52, Def2;
then y,c' // a,c' by A43, A41, AFF_1:14;
then c',y // c',a by AFF_1:13;
then LIN c',y,a by AFF_1:def 1;
then A56: LIN a,y,c' by AFF_1:15;
LIN a,y,b' 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;