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 A6, A7, A8, A10, AFF_1:45;
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 A16, AFF_1:24;
A20: not K // N
proof
assume K // N ; :: thesis: contradiction
then Line (c,b9) // N by A18, AFF_1:44;
then Line (c,b9) // M by A7, AFF_1:44;
then b9 in M by A6, A19, AFF_1:45;
hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum
end;
K is being_line by A18, AFF_1:36;
then consider x being Element of AP such that
A21: x in K and
A22: x in N by A3, A20, AFF_1:58;
A23: b,x // c,b9 by A19, A17, A18, A21, AFF_1:39;
then a,x // c,a9 by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A22;
then a,x // a,c9 by A13, A15, AFF_1:5;
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 A11, AFF_1:def 1;
then LIN a9,b9,a by AFF_1:6;
then ( a9 = b9 or a in N ) by A3, A9, A10, AFF_1:25;
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 A12, A16, A23, AFF_1:5;
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 A33, A35, A38, AFF_1:45;
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 A44, AFF_1:24;
A47: Line (c,a9) is being_line by A44, AFF_1:24;
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 A39, AFF_1:4;
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 A30, A32, A33, AFF_1:25;
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 A40, A41, A42, AFF_1:32, AFF_1:40;
then c,b9 // Line (c,a9) by A49, AFF_1:43;
then b9 in Line (c,a9) by A47, A45, AFF_1:23;
then c in N by A31, A36, A37, A50, A47, A45, A46, AFF_1:18;
hence contradiction by A34, A35, AFF_1:45; :: thesis: verum
end;
A53: Line (b,c9) is being_line by A41, AFF_1:24;
P is being_line by A49, AFF_1:36;
then consider x being Element of AP such that
A54: x in Line (b,c9) and
A55: x in P by A53, A52, AFF_1:58;
LIN b,x,c9 by A53, A42, A54, AFF_1:21;
then b,x // b,c9 by AFF_1:def 1;
then A56: b,x // c,b9 by A40, A41, AFF_1:5;
a,x // c,a9 by A45, A46, A48, A49, A55, AFF_1:39;
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 A31, A38, A53, A42, A54, AFF_1:18;
hence contradiction by A33, A35, A43, A45, A46, A48, A49, A55, AFF_1:39, AFF_1:45; :: thesis: verum