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, 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 & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & a9 <> b9 holds
c9 in N
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 & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & a9 <> b9 holds
c9 in N
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 & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & a9 <> b9 implies c9 in N )
assume that
A3: M is being_line and
A4: N is being_line and
A5: a in M and
A6: b in M and
A7: c in M and
A8: M // N and
A9: M <> N and
A10: a9 in N and
A11: b9 in N and
A12: a,b9 // b,a9 and
A13: b,c9 // c,b9 and
A14: a,c9 // c,a9 and
A15: a9 <> b9 ; :: thesis: c9 in N
A16: c <> a9 by A7, A8, A9, A10, AFF_1:59;
set C = Line c,b9;
A17: c <> b9 by A7, A8, A9, A11, AFF_1:59;
then Line c,b9 is being_line by AFF_1:38;
then consider K being Subset of AP such that
A18: b in K and
A19: Line c,b9 // K by AFF_1:63;
A20: ( c in Line c,b9 & b9 in Line c,b9 ) by A17, AFF_1:38;
A21: not K // N

proof

assume K // N ; :: thesis: contradiction
then Line c,b9 // N by A19, AFF_1:58;
then Line c,b9 // M by A8, AFF_1:58;
then b9 in M by A7, A20, AFF_1:59;
hence contradiction by A8, A9, A11, AFF_1:59; :: thesis: verum

end;

K is being_line by A19, AFF_1:50;
then consider x being Element of AP such that
A22: x in K and
A23: x in N by A4, A21, AFF_1:72;
A24: b,x // c,b9 by A20, A18, A19, A22, AFF_1:53;
then a,x // c,a9 by A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A23, Def13;
then a,x // a,c9 by A14, A16, AFF_1:14;
then LIN a,x,c9 by AFF_1:def 1;
then A25: LIN c9,x,a by AFF_1:15;
A26: a <> b

proof

assume 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 A4, A10, A11, AFF_1:39;
hence contradiction by A5, A8, A9, A15, AFF_1:59; :: thesis: verum

end;

A27: c9 <> b

proof

assume c9 = b ; :: thesis: contradiction
then a9 in M by A3, A5, A6, A7, A14, A26, AFF_1:62;
hence contradiction by A8, A9, A10, AFF_1:59; :: thesis: verum

end;

b,x // b,c9 by A13, A17, A24, AFF_1:14;
then LIN b,x,c9 by AFF_1:def 1;
then A28: LIN c9,x,b by AFF_1:15;
assume A29: not c9 in N ; :: thesis: contradiction
LIN c9,x,c9 by AFF_1:16;
then c9 in M by A3, A5, A6, A29, A26, A23, A25, A28, AFF_1:17, AFF_1:39;
then b9 in M by A3, A6, A7, A13, A27, AFF_1:62;
hence contradiction by A8, A9, A11, AFF_1:59; :: thesis: verum

end;

end;

now

assume A30: 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, 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
A31: M is being_line and
A32: N is being_line and
A33: a in M and
A34: b in M and
A35: c in M and
A36: ( M // N & M <> N ) and
A37: a9 in N and
A38: b9 in N and
A39: c9 in N and
A40: a,b9 // b,a9 and
A41: b,c9 // c,b9 ; :: thesis: a,c9 // c,a9
set A = Line c,a9;
set C = Line c,b9;
set D = Line b,c9;
A42: b <> c9 by A34, A36, A39, AFF_1:59;
then A43: ( b in Line b,c9 & c9 in Line b,c9 ) by AFF_1:38;
assume A44: not a,c9 // c,a9 ; :: thesis: contradiction
then A45: c <> a9 by AFF_1:12;
then A46: c in Line c,a9 by AFF_1:38;
A47: a9 in Line c,a9 by A45, AFF_1:38;
A48: Line c,a9 is being_line by A45, AFF_1:38;
then consider P being Subset of AP such that
A49: a in P and
A50: Line c,a9 // P by AFF_1:63;
A51: a9 <> b9

proof

assume A52: a9 = b9 ; :: thesis: contradiction
then a9,a // a9,b by A40, AFF_1:13;
then LIN a9,a,b by AFF_1:def 1;
then LIN a,b,a9 by AFF_1:15;
then ( a = b or a9 in M ) by A31, A33, A34, AFF_1:39;
hence contradiction by A36, A37, A41, A44, A52, AFF_1:59; :: thesis: verum

end;

A53: not Line b,c9 // P

proof

assume Line b,c9 // P ; :: thesis: contradiction
then c,b9 // P by A41, A42, A43, AFF_1:46, AFF_1:54;
then c,b9 // Line c,a9 by A50, AFF_1:57;
then b9 in Line c,a9 by A48, A46, AFF_1:37;
then c in N by A32, A37, A38, A51, A48, A46, A47, AFF_1:30;
hence contradiction by A35, A36, AFF_1:59; :: thesis: verum

end;

A54: Line b,c9 is being_line by A42, AFF_1:38;
P is being_line by A50, AFF_1:50;
then consider x being Element of AP such that
A55: x in Line b,c9 and
A56: x in P by A54, A53, AFF_1:72;
LIN b,x,c9 by A54, A43, A55, AFF_1:33;
then b,x // b,c9 by AFF_1:def 1;
then A57: b,x // c,b9 by A41, A42, AFF_1:14;
a,x // c,a9 by A46, A47, A49, A50, A56, AFF_1:53;
then x in N by A30, A31, A32, A33, A34, A35, A36, A37, A38, A40, A51, A57, Def14;
then ( x = c9 or b in N ) by A32, A39, A54, A43, A55, AFF_1:30;
hence contradiction by A34, A36, A44, A46, A47, A49, A50, A56, 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