let AP be AffinPlane; :: thesis: ( AP is satisfying_pap iff AP is satisfying_pap_1 )
hereby :: thesis: ( AP is satisfying_pap_1 implies AP is satisfying_pap )
assume A1: 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
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: a,b9 // b,a9 and
A12: b,c9 // c,b9 and
A13: a,c9 // c,a9 and
A14: a9 <> b9 ; :: thesis: c9 in N
A15: c <> a9 by A6, A7, A8, A9, AFF_1:45;
set C = Line (c,b9);
A16: c <> b9 by ;
then Line (c,b9) is being_line by AFF_1:24;
then consider K being Subset of AP such that
A17: b in K and
A18: Line (c,b9) // K by AFF_1:49;
A19: ( c in Line (c,b9) & b9 in Line (c,b9) ) by ;
A20: not K // N
proof
assume K // N ; :: thesis: contradiction
then Line (c,b9) // N by ;
then Line (c,b9) // M by ;
then b9 in M by ;
hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum
end;
K is being_line by ;
then consider x being Element of AP such that
A21: x in K and
A22: x in N by ;
A23: b,x // c,b9 by ;
then a,x // c,a9 by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A22;
then a,x // a,c9 by ;
then LIN a,x,c9 by AFF_1:def 1;
then A24: LIN c9,x,a by AFF_1:6;
A25: a <> b
proof
assume a = b ; :: thesis: contradiction
then LIN a,b9,a9 by ;
then LIN a9,b9,a by AFF_1:6;
then ( a9 = b9 or a in N ) by ;
hence contradiction by A4, A7, A8, A14, AFF_1:45; :: thesis: verum
end;
A26: c9 <> b
proof
assume c9 = b ; :: thesis: contradiction
then a9 in M by A2, A4, A5, A6, A13, A25, AFF_1:48;
hence contradiction by A7, A8, A9, AFF_1:45; :: thesis: verum
end;
b,x // b,c9 by ;
then LIN b,x,c9 by AFF_1:def 1;
then A27: LIN c9,x,b by AFF_1:6;
assume A28: not c9 in N ; :: thesis: contradiction
LIN c9,x,c9 by AFF_1:7;
then c9 in M by A2, A4, A5, A28, A25, A22, A24, A27, AFF_1:8, AFF_1:25;
then b9 in M by A2, A5, A6, A12, A26, AFF_1:48;
hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum
end;
end;
assume A29: AP is satisfying_pap_1 ; :: thesis: AP is satisfying_pap
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
A30: M is being_line and
A31: N is being_line and
A32: a in M and
A33: b in M and
A34: c in M and
A35: ( M // N & M <> N ) and
A36: a9 in N and
A37: b9 in N and
A38: c9 in N and
A39: a,b9 // b,a9 and
A40: b,c9 // c,b9 ; :: thesis: a,c9 // c,a9
set A = Line (c,a9);
set D = Line (b,c9);
A41: b <> c9 by ;
then A42: ( b in Line (b,c9) & c9 in Line (b,c9) ) by AFF_1:24;
assume A43: not a,c9 // c,a9 ; :: thesis: contradiction
then A44: c <> a9 by AFF_1:3;
then A45: c in Line (c,a9) by AFF_1:24;
A46: a9 in Line (c,a9) by ;
A47: Line (c,a9) is being_line by ;
then consider P being Subset of AP such that
A48: a in P and
A49: Line (c,a9) // P by AFF_1:49;
A50: a9 <> b9
proof
assume A51: a9 = b9 ; :: thesis: contradiction
then a9,a // a9,b by ;
then LIN a9,a,b by AFF_1:def 1;
then LIN a,b,a9 by AFF_1:6;
then ( a = b or a9 in M ) by ;
hence contradiction by A35, A36, A40, A43, A51, AFF_1:45; :: thesis: verum
end;
A52: not Line (b,c9) // P
proof
assume Line (b,c9) // P ; :: thesis: contradiction
then c,b9 // P by ;
then c,b9 // Line (c,a9) by ;
then b9 in Line (c,a9) by ;
then c in N by ;
hence contradiction by A34, A35, AFF_1:45; :: thesis: verum
end;
A53: Line (b,c9) is being_line by ;
P is being_line by ;
then consider x being Element of AP such that
A54: x in Line (b,c9) and
A55: x in P by ;
LIN b,x,c9 by ;
then b,x // b,c9 by AFF_1:def 1;
then A56: b,x // c,b9 by ;
a,x // c,a9 by ;
then x in N by A29, A30, A31, A32, A33, A34, A35, A36, A37, A39, A50, A56;
then ( x = c9 or b in N ) by ;
hence contradiction by A33, A35, A43, A45, A46, A48, A49, A55, AFF_1:39, AFF_1:45; :: thesis: verum