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, a', b', c' 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 & 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 AP; :: thesis: for a, b, c, a', b', c' 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 & 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 AP; :: 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 A2: ( 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: a,c' // c,a'
assume A3: not a,c' // c,a' ; :: thesis: contradiction
A4: ( a <> b' & c <> b' & b <> c' & b <> a' & a <> c' ) by A2, AFF_1:59;
A5: ( a <> b & a <> c & b <> c )

proof

A6: now

assume A7: a = b ; :: thesis: contradiction
then LIN a,b',a' by A2, AFF_1:def 1;
then LIN a',b',a by AFF_1:15;
then ( a' = b' or a in N ) by A2, AFF_1:39;
hence contradiction by A2, A3, A7, AFF_1:59; :: thesis: verum

end;

A8: now

assume A9: a = c ; :: thesis: contradiction
then b,c' // b,a' by A2, A4, AFF_1:14;
then LIN b,c',a' by AFF_1:def 1;
then LIN a',c',b by AFF_1:15;
then ( a' = c' or b in N ) by A2, AFF_1:39;
hence contradiction by A2, A3, A9, AFF_1:11, AFF_1:59; :: thesis: verum

end;

now

assume A10: b = c ; :: thesis: contradiction
then LIN b,c',b' by A2, AFF_1:def 1;
then LIN b',c',b by AFF_1:15;
then ( b' = c' or b in N ) by A2, AFF_1:39;
hence contradiction by A2, A3, A10, AFF_1:59; :: thesis: verum

end;

hence ( a <> b & a <> c & b <> c ) by A6, A8; :: thesis: verum

end;

A11: ( a' <> b' & a' <> c' & b' <> c' )

proof

A12: now

assume a' = b' ; :: thesis: contradiction
then a',a // a',b by A2, 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, A5, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

A13: now

assume a' = c' ; :: thesis: contradiction
then a,b' // c,b' by A2, A4, AFF_1:14;
then b',a // b',c by AFF_1:13;
then LIN b',a,c by AFF_1:def 1;
then LIN a,c,b' by AFF_1:15;
then b' in M by A2, A5, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

now

assume b' = c' ; :: thesis: contradiction
then b',b // b',c by A2, 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, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

hence ( a' <> b' & a' <> c' & b' <> c' ) by A12, A13; :: thesis: verum

end;

set K = Line a,c';
set C = Line c,b';
A14: ( Line a,c' is being_line & Line c,b' is being_line & a in Line a,c' & c' in Line a,c' & c in Line c,b' & b' in Line c,b' ) by A4, AFF_1:38;
then consider T being Subset of AP such that
A15: ( a' in T & Line a,c' // T ) by AFF_1:63;
A16: ( T is being_line & T // Line a,c' ) by A15, AFF_1:50;
not Line c,b' // T

proof

assume Line c,b' // T ; :: thesis: contradiction
then Line c,b' // Line a,c' by A15, AFF_1:58;
then c,b' // a,c' by A14, AFF_1:53;
then b,c' // a,c' by A2, A4, 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, A5, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

then consider x being Element of AP such that
A17: ( x in Line c,b' & x in T ) by A14, A16, AFF_1:72;
A18: a,c' // x,a' by A14, A15, A17, AFF_1:53;
A19: x <> b

proof

assume x = b ; :: thesis: contradiction
then LIN b,c,b' by A14, A17, AFF_1:33;
then b' in M by A2, A5, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

set D = Line x,b;
A20: ( Line x,b is being_line & x in Line x,b & b in Line x,b ) by A19, AFF_1:38;
not Line x,b // N

proof

assume Line x,b // N ; :: thesis: contradiction
then Line x,b // M by A2, AFF_1:58;
then x in M by A2, A20, AFF_1:59;
then ( c in T or b' in M ) by A2, A14, A17, AFF_1:30;
hence contradiction by A2, A3, A14, A15, AFF_1:53, AFF_1:59; :: thesis: verum

end;

then consider o being Element of AP such that
A21: ( o in Line x,b & o in N ) by A2, A20, AFF_1:72;
A22: b,c' // x,b'

proof

LIN b',c,x by A14, A17, AFF_1:33;
then b',c // b',x by AFF_1:def 1;
then c,b' // x,b' by AFF_1:13;
hence b,c' // x,b' by A2, A4, AFF_1:14; :: thesis: verum

end;

A23: a' <> x

proof

assume a' = x ; :: thesis: contradiction
then c,b' // a',b' by A2, A4, A22, AFF_1:14;
then b',a' // b',c by AFF_1:13;
then LIN b',a',c by AFF_1:def 1;
then c in N by A2, A11, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

A24: b' <> x

proof

assume b' = x ; :: thesis: contradiction
then a,c' // a',b' by A14, A15, A17, AFF_1:53;
then a,c' // N by A2, A11, AFF_1:41;
then c',a // N by AFF_1:48;
then a in N by A2, AFF_1:37;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

not a,b' // Line x,b

proof

assume a,b' // Line x,b ; :: thesis: contradiction
then b,a' // Line x,b by A2, A4, AFF_1:46;
then a' in Line x,b by A20, AFF_1:37;
then b in T by A15, A16, A17, A20, A23, AFF_1:30;
then b,a' // a,c' by A14, A15, AFF_1:53;
then a,b' // a,c' by A2, A4, 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 A2, A11, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

then consider y being Element of AP such that
A25: ( y in Line x,b & LIN a,b',y ) by A20, AFF_1:73;
A26: y,b' // b,a'

proof

LIN b',a,y by A25, AFF_1:15;
then b',a // b',y by AFF_1:def 1;
then a,b' // y,b' by AFF_1:13;
hence y,b' // b,a' by A2, A4, AFF_1:14; :: thesis: verum

end;

A27: Line x,b <> N by A2, A20, AFF_1:59;
A28: ( o <> b' & o <> c' & o <> a' )

proof

A29: now

assume o = b' ; :: thesis: contradiction
then LIN b',x,b by A20, A21, 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 A22, A24, 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 A2, A11, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

A30: now

assume o = a' ; :: thesis: contradiction
then LIN a',b,x by A20, A21, 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 A2, A4, AFF_1:14;
then a,b' // a,c' by A18, A23, 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 A2, A11, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

now

assume o = c' ; :: thesis: contradiction
then Line x,b // Line c,b' by A2, A4, A14, A20, A21, AFF_1:52;
then b in Line c,b' by A17, A20, AFF_1:59;
then LIN c,b,b' by A14, AFF_1:33;
then b' in M by A2, A5, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

hence ( o <> b' & o <> c' & o <> a' ) by A29, A30; :: thesis: verum

end;

( o <> b & o <> x & o <> y )

proof

A31: now

assume o = x ; :: thesis: contradiction
then N = T by A2, A15, A16, A17, A21, A23, AFF_1:30;
then N = Line a,c' by A2, A14, A15, AFF_1:59;
hence contradiction by A2, A14, AFF_1:59; :: thesis: verum

end;

now

assume o = y ; :: thesis: contradiction
then ( LIN b',o,a & LIN b',o,a' & LIN b',o,b' ) by A2, A21, A25, AFF_1:15, AFF_1:33;
then a in N by A2, A11, A28, AFF_1:17, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

hence ( o <> b & o <> x & o <> y ) by A2, A21, A31, AFF_1:59; :: thesis: verum

end;

then y,c' // x,a' by A1, A2, A20, A21, A22, A25, A26, A27, A28, Def2;
then y,c' // a,c' by A18, A23, AFF_1:14;
then c',y // c',a by AFF_1:13;
then LIN c',y,a by AFF_1:def 1;
then ( LIN a,y,c' & LIN a,y,b' & LIN a,y,a ) by A25, AFF_1:15, AFF_1:16;
then ( a in Line x,b or a in N ) by A2, A11, A25, AFF_1:17, AFF_1:39;
then Line x,b // N by A2, A5, A20, AFF_1:30, AFF_1:59;
hence contradiction by A21, A27, AFF_1:59; :: thesis: verum

end;