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