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