let AP be AffinPlane; :: thesis: ( AP is satisfying_pap iff AP is satisfying_pap_1 )

A1: now

assume A2: AP is satisfying_pap ; :: thesis: AP is satisfying_pap_1
thus AP is satisfying_pap_1 :: thesis: verum

proof

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

proof

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

end;

set C = Line c,b';
A8: ( Line c,b' is being_line & c in Line c,b' & b' in Line c,b' ) by A5, AFF_1:38;
then consider K being Subset of AP such that
A9: ( b in K & Line c,b' // K ) by AFF_1:63;
A10: ( K is being_line & K // Line c,b' ) by A9, AFF_1:50;
not K // N

proof

assume K // N ; :: thesis: contradiction
then ( Line c,b' // N & N // M ) by A3, A9, AFF_1:58;
then Line c,b' // M by AFF_1:58;
then b' in M by A3, A8, AFF_1:59;
hence contradiction by A3, AFF_1:59; :: thesis: verum

end;

then consider x being Element of AP such that
A11: ( x in K & x in N ) by A3, A10, AFF_1:72;
A12: c' <> b

proof

assume c' = b ; :: thesis: contradiction
then a' in M by A3, A7, AFF_1:62;
hence contradiction by A3, AFF_1:59; :: thesis: verum

end;

A13: b,x // c,b' by A8, A9, A11, AFF_1:53;
then a,x // c,a' by A2, A3, A11, Def13;
then a,x // a,c' by A3, A6, AFF_1:14;
then A14: LIN a,x,c' by AFF_1:def 1;
b,x // b,c' by A3, A5, A13, AFF_1:14;
then LIN b,x,c' by AFF_1:def 1;
then ( LIN c',x,a & LIN c',x,b & LIN c',x,c' ) by A14, AFF_1:15, AFF_1:16;
then c' in M by A3, A4, A7, A11, AFF_1:17, AFF_1:39;
then b' in M by A3, A12, AFF_1:62;
hence contradiction by A3, AFF_1:59; :: thesis: verum

end;

end;

now

assume A15: AP is satisfying_pap_1 ; :: 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 A16: ( 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 A17: not a,c' // c,a' ; :: thesis: contradiction
then A18: ( a <> c' & c <> a' ) by AFF_1:12;
set A = Line c,a';
set C = Line c,b';
set D = Line b,c';
A19: ( c <> b' & b <> c' ) by A16, AFF_1:59;
A20: a' <> b'

proof

assume A21: a' = b' ; :: thesis: contradiction
then a',a // a',b by A16, AFF_1:13;
then LIN a',a,b by AFF_1:def 1;
then LIN a,b,a' by AFF_1:15;
then ( a = b or a' in M ) by A16, AFF_1:39;
hence contradiction by A16, A17, A21, AFF_1:59; :: thesis: verum

end;

A22: ( Line c,a' is being_line & Line c,b' is being_line & Line b,c' is being_line & c in Line c,a' & a' in Line c,a' & c in Line c,b' & b' in Line c,b' & b in Line b,c' & c' in Line b,c' ) by A18, A19, AFF_1:38;
then consider P being Subset of AP such that
A23: ( a in P & Line c,a' // P ) by AFF_1:63;
A24: ( P is being_line & P // Line c,a' ) by A23, AFF_1:50;
not Line b,c' // P

proof

assume Line b,c' // P ; :: thesis: contradiction
then c,b' // P by A16, A19, A22, AFF_1:46, AFF_1:54;
then c,b' // Line c,a' by A23, AFF_1:57;
then b' in Line c,a' by A22, AFF_1:37;
then c in N by A16, A20, A22, AFF_1:30;
hence contradiction by A16, AFF_1:59; :: thesis: verum

end;

then consider x being Element of AP such that
A25: ( x in Line b,c' & x in P ) by A22, A24, AFF_1:72;
A26: a,x // c,a' by A22, A23, A25, AFF_1:53;
b,x // c,b'

proof

LIN b,x,c' by A22, A25, AFF_1:33;
then b,x // b,c' by AFF_1:def 1;
hence b,x // c,b' by A16, A19, AFF_1:14; :: thesis: verum

end;

then x in N by A15, A16, A20, A26, Def14;
then ( x = c' or b in N ) by A16, A22, A25, AFF_1:30;
hence contradiction by A16, A17, A22, A23, A25, AFF_1:53, AFF_1:59; :: thesis: verum

end;

end;

hence ( AP is satisfying_pap iff AP is satisfying_pap_1 ) by A1; :: thesis: verum