let AP be AffinPlane; :: thesis: ( AP is Pappian implies AP is Desarguesian )
assume A1: AP is Pappian ; :: thesis: AP is Desarguesian
then AP is satisfying_pap by Th9;
then A2: AP is satisfying_PPAP by A1, Th10;
let A be Subset of AP; :: according to AFF_2:def 4 :: thesis: for P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let P, C be Subset of AP; :: thesis: for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let o, a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
assume that
A3: o in A and
A4: o in P and
A5: o in C and
A6: o <> a and
A7: o <> b and
o <> c and
A8: a in A and
A9: a9 in A and
A10: b in P and
A11: b9 in P and
A12: c in C and
A13: c9 in C and
A14: A is being_line and
A15: P is being_line and
A16: C is being_line and
A17: A <> P and
A18: A <> C and
A19: a,b // a9,b9 and
A20: a,c // a9,c9 ; :: thesis: b,c // b9,c9
assume A21: not b,c // b9,c9 ; :: thesis: contradiction
then A22: b <> c by AFF_1:3;
A23: a <> c by A3, A5, A6, A8, A12, A14, A16, A18, AFF_1:18;
A24: not b in C
proof
assume A25: b in C ; :: thesis: contradiction
then b9 in C by A4, A5, A7, A10, A11, A15, A16, AFF_1:18;
hence contradiction by A12, A13, A16, A21, A25, AFF_1:51; :: thesis: verum
end;
A26: a <> b by A3, A4, A6, A8, A10, A14, A15, A17, AFF_1:18;
A27: a <> a9
proof
assume A28: a = a9 ; :: thesis: contradiction
then LIN a,c,c9 by A20, AFF_1:def 1;
then LIN c,c9,a by AFF_1:6;
then A29: ( c = c9 or a in C ) by A12, A13, A16, AFF_1:25;
LIN a,b,b9 by A19, A28, AFF_1:def 1;
then LIN b,b9,a by AFF_1:6;
then ( b = b9 or a in P ) by A10, A11, A15, AFF_1:25;
hence contradiction by A3, A4, A5, A6, A8, A14, A15, A16, A17, A18, A21, A29, AFF_1:2, AFF_1:18; :: thesis: verum
end;
set M = Line (b9,c9);
set N = Line (a9,b9);
set D = Line (a9,c9);
A30: a9 <> b9
proof
A31: a9,c9 // c,a by A20, AFF_1:4;
assume A32: a9 = b9 ; :: thesis: contradiction
then a9 in C by A3, A4, A5, A9, A11, A14, A15, A17, AFF_1:18;
then ( a in C or a9 = c9 ) by A12, A13, A16, A31, AFF_1:48;
hence contradiction by A3, A5, A6, A8, A14, A16, A18, A21, A32, AFF_1:3, AFF_1:18; :: thesis: verum
end;
then A33: Line (a9,b9) is being_line by AFF_1:24;
A34: a9 <> c9
proof
assume a9 = c9 ; :: thesis: contradiction
then A35: a9 in P by A3, A4, A5, A9, A13, A14, A16, A18, AFF_1:18;
a9,b9 // b,a by A19, AFF_1:4;
then a in P by A10, A11, A15, A30, A35, AFF_1:48;
hence contradiction by A3, A4, A6, A8, A14, A15, A17, AFF_1:18; :: thesis: verum
end;
A36: not LIN a9,b9,c9
proof
assume A37: LIN a9,b9,c9 ; :: thesis: contradiction
then a9,b9 // a9,c9 by AFF_1:def 1;
then a9,b9 // a,c by A20, A34, AFF_1:5;
then a,b // a,c by A19, A30, AFF_1:5;
then LIN a,b,c by AFF_1:def 1;
then LIN b,c,a by AFF_1:6;
then b,c // b,a by AFF_1:def 1;
then b,c // a,b by AFF_1:4;
then A38: b,c // a9,b9 by A19, A26, AFF_1:5;
LIN b9,c9,a9 by A37, AFF_1:6;
then b9,c9 // b9,a9 by AFF_1:def 1;
then b9,c9 // a9,b9 by AFF_1:4;
hence contradiction by A21, A30, A38, AFF_1:5; :: thesis: verum
end;
A39: not LIN a,b,c
proof
assume LIN a,b,c ; :: thesis: contradiction
then a,b // a,c by AFF_1:def 1;
then a,b // a9,c9 by A20, A23, AFF_1:5;
then a9,b9 // a9,c9 by A19, A26, AFF_1:5;
hence contradiction by A36, AFF_1:def 1; :: thesis: verum
end;
A40: now :: thesis: b,c // A
LIN o,a,a9 by A3, A8, A9, A14, AFF_1:21;
then o,a // o,a9 by AFF_1:def 1;
then A41: a9,o // a,o by AFF_1:4;
set M = Line (b,c);
set N = Line (a,b);
set D = Line (a,c);
A42: Line (a,b) is being_line by A26, AFF_1:24;
Line (b,c) is being_line by A22, AFF_1:24;
then consider K being Subset of AP such that
A43: o in K and
A44: Line (b,c) // K by AFF_1:49;
A45: K is being_line by A44, AFF_1:36;
A46: a in Line (a,b) by A26, AFF_1:24;
A47: b in Line (a,b) by A26, AFF_1:24;
A48: ( b in Line (b,c) & c in Line (b,c) ) by A22, AFF_1:24;
not Line (a,b) // K
proof
assume Line (a,b) // K ; :: thesis: contradiction
then Line (a,b) // Line (b,c) by A44, AFF_1:44;
then c in Line (a,b) by A48, A47, AFF_1:45;
hence contradiction by A39, A42, A46, A47, AFF_1:21; :: thesis: verum
end;
then consider p being Element of AP such that
A49: p in Line (a,b) and
A50: p in K by A42, A45, AFF_1:58;
A51: b,c // p,o by A48, A43, A44, A50, AFF_1:39;
A52: o <> p
proof
assume o = p ; :: thesis: contradiction
then LIN o,a,b by A42, A46, A47, A49, AFF_1:21;
then b in A by A3, A6, A8, A14, AFF_1:25;
hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:18; :: thesis: verum
end;
set R = Line (a9,p);
A53: p <> a9
proof
assume p = a9 ; :: thesis: contradiction
then b in A by A8, A9, A14, A27, A42, A46, A47, A49, AFF_1:18;
hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:18; :: thesis: verum
end;
then A54: Line (a9,p) is being_line by AFF_1:24;
Line (a,c) is being_line by A23, AFF_1:24;
then consider T being Subset of AP such that
A55: p in T and
A56: Line (a,c) // T by AFF_1:49;
A57: ( a in Line (a,c) & c in Line (a,c) ) by A23, AFF_1:24;
A58: not C // T
proof
assume C // T ; :: thesis: contradiction
then C // Line (a,c) by A56, AFF_1:44;
then a in C by A12, A57, AFF_1:45;
hence contradiction by A3, A5, A6, A8, A14, A16, A18, AFF_1:18; :: thesis: verum
end;
T is being_line by A56, AFF_1:36;
then consider q being Element of AP such that
A59: q in C and
A60: q in T by A16, A58, AFF_1:58;
A61: p,q // a,c by A57, A55, A56, A60, AFF_1:39;
then A62: b,q // a,o by A2, A5, A12, A16, A42, A46, A47, A49, A59, A51;
A63: ( a9 in Line (a9,p) & p in Line (a9,p) ) by A53, AFF_1:24;
assume not b,c // A ; :: thesis: contradiction
then A64: K <> A by A48, A44, AFF_1:40;
not b,q // Line (a9,p)
proof
assume b,q // Line (a9,p) ; :: thesis: contradiction
then A65: a,o // Line (a9,p) by A24, A59, A62, AFF_1:32;
a,o // A by A3, A8, A14, AFF_1:40, AFF_1:41;
then p in A by A6, A9, A63, A65, AFF_1:45, AFF_1:53;
hence contradiction by A3, A14, A43, A45, A50, A52, A64, AFF_1:18; :: thesis: verum
end;
then consider r being Element of AP such that
A66: r in Line (a9,p) and
A67: LIN b,q,r by A54, AFF_1:59;
A68: now :: thesis: ( r = q implies r,b // o,a9 )
assume r = q ; :: thesis: r,b // o,a9
then b,r // a,o by A2, A5, A12, A16, A42, A46, A47, A49, A59, A51, A61;
then A69: r,b // o,a by AFF_1:4;
LIN o,a,a9 by A3, A8, A9, A14, AFF_1:21;
then o,a // o,a9 by AFF_1:def 1;
hence r,b // o,a9 by A6, A69, AFF_1:5; :: thesis: verum
end;
LIN q,r,b by A67, AFF_1:6;
then q,r // q,b by AFF_1:def 1;
then r,q // b,q by AFF_1:4;
then r,q // a,o by A24, A59, A62, AFF_1:5;
then A70: a9,o // r,q by A6, A41, AFF_1:5;
LIN b,a,p by A42, A46, A47, A49, AFF_1:21;
then b,a // b,p by AFF_1:def 1;
then a,b // p,b by AFF_1:4;
then A71: p,b // a9,b9 by A19, A26, AFF_1:5;
LIN r,b,q by A67, AFF_1:6;
then r,b // r,q by AFF_1:def 1;
then a9,o // r,b by A70, A68, AFF_1:4, AFF_1:5;
then A72: p,o // r,b9 by A2, A4, A10, A11, A15, A54, A63, A66, A71;
p,q // a9,c9 by A20, A23, A61, AFF_1:5;
then A73: p,o // r,c9 by A2, A5, A13, A16, A59, A54, A63, A66, A70;
then r,c9 // r,b9 by A52, A72, AFF_1:5;
then LIN r,c9,b9 by AFF_1:def 1;
then LIN c9,b9,r by AFF_1:6;
then c9,b9 // c9,r by AFF_1:def 1;
then A74: r,c9 // b9,c9 by AFF_1:4;
b,c // r,c9 by A52, A51, A73, AFF_1:5;
then r = c9 by A21, A74, AFF_1:5;
then p,o // b9,c9 by A72, AFF_1:4;
hence contradiction by A21, A52, A51, AFF_1:5; :: thesis: verum
end;
A75: b9 in Line (a9,b9) by A30, AFF_1:24;
A76: b9 <> c9 by A21, AFF_1:3;
then A77: ( b9 in Line (b9,c9) & c9 in Line (b9,c9) ) by AFF_1:24;
Line (b9,c9) is being_line by A76, AFF_1:24;
then consider K being Subset of AP such that
A78: o in K and
A79: Line (b9,c9) // K by AFF_1:49;
A80: K is being_line by A79, AFF_1:36;
A81: a9 in Line (a9,b9) by A30, AFF_1:24;
not Line (a9,b9) // K
proof
assume Line (a9,b9) // K ; :: thesis: contradiction
then Line (a9,b9) // Line (b9,c9) by A79, AFF_1:44;
then c9 in Line (a9,b9) by A77, A75, AFF_1:45;
hence contradiction by A36, A33, A81, A75, AFF_1:21; :: thesis: verum
end;
then consider p being Element of AP such that
A82: p in Line (a9,b9) and
A83: p in K by A33, A80, AFF_1:58;
A84: o <> a9
proof
assume A85: o = a9 ; :: thesis: contradiction
a9,b9 // b,a by A19, AFF_1:4;
then a in P by A4, A10, A11, A15, A30, A85, AFF_1:48;
hence contradiction by A3, A4, A6, A8, A14, A15, A17, AFF_1:18; :: thesis: verum
end;
A86: o <> p
proof
assume o = p ; :: thesis: contradiction
then LIN o,a9,b9 by A33, A81, A75, A82, AFF_1:21;
then A87: b9 in A by A3, A9, A14, A84, AFF_1:25;
a9,b9 // a,b by A19, AFF_1:4;
then b in A by A8, A9, A14, A30, A87, AFF_1:48;
hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:18; :: thesis: verum
end;
Line (a9,c9) is being_line by A34, AFF_1:24;
then consider T being Subset of AP such that
A88: p in T and
A89: Line (a9,c9) // T by AFF_1:49;
A90: T is being_line by A89, AFF_1:36;
A91: ( a9 in Line (a9,c9) & c9 in Line (a9,c9) ) by A34, AFF_1:24;
not C // T
proof
assume C // T ; :: thesis: contradiction
then C // Line (a9,c9) by A89, AFF_1:44;
then a9 in C by A13, A91, AFF_1:45;
hence contradiction by A3, A5, A9, A14, A16, A18, A84, AFF_1:18; :: thesis: verum
end;
then consider q being Element of AP such that
A92: q in C and
A93: q in T by A16, A90, AFF_1:58;
A94: b9,c9 // p,o by A77, A78, A79, A83, AFF_1:39;
A95: o <> b9
proof
assume A96: o = b9 ; :: thesis: contradiction
b9,a9 // a,b by A19, AFF_1:4;
then b in A by A3, A8, A9, A14, A30, A96, AFF_1:48;
hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:18; :: thesis: verum
end;
A97: b9 <> q
proof
assume b9 = q ; :: thesis: contradiction
then P = C by A4, A5, A11, A15, A16, A95, A92, AFF_1:18;
hence contradiction by A10, A11, A12, A13, A15, A21, AFF_1:51; :: thesis: verum
end;
set R = Line (a,p);
A98: p <> a
proof
assume p = a ; :: thesis: contradiction
then b9 in A by A8, A9, A14, A27, A33, A81, A75, A82, AFF_1:18;
hence contradiction by A3, A4, A11, A14, A15, A17, A95, AFF_1:18; :: thesis: verum
end;
then A99: Line (a,p) is being_line by AFF_1:24;
A100: p,q // a9,c9 by A91, A88, A89, A93, AFF_1:39;
then A101: b9,q // a9,o by A2, A5, A13, A16, A33, A81, A75, A82, A92, A94;
A102: ( a in Line (a,p) & p in Line (a,p) ) by A98, AFF_1:24;
not b9,c9 // A by A14, A21, A40, AFF_1:31;
then A103: K <> A by A77, A79, AFF_1:40;
not b9,q // Line (a,p)
proof
assume b9,q // Line (a,p) ; :: thesis: contradiction
then A104: a9,o // Line (a,p) by A101, A97, AFF_1:32;
a9,o // A by A3, A9, A14, AFF_1:40, AFF_1:41;
then p in A by A8, A84, A102, A104, AFF_1:45, AFF_1:53;
hence contradiction by A3, A14, A78, A80, A83, A86, A103, AFF_1:18; :: thesis: verum
end;
then consider r being Element of AP such that
A105: r in Line (a,p) and
A106: LIN b9,q,r by A99, AFF_1:59;
A107: now :: thesis: ( r = q implies r,b9 // o,a )
assume r = q ; :: thesis: r,b9 // o,a
then b9,r // a9,o by A2, A5, A13, A16, A33, A81, A75, A82, A92, A94, A100;
then A108: r,b9 // o,a9 by AFF_1:4;
LIN o,a9,a by A3, A8, A9, A14, AFF_1:21;
then o,a9 // o,a by AFF_1:def 1;
hence r,b9 // o,a by A84, A108, AFF_1:5; :: thesis: verum
end;
LIN b9,a9,p by A33, A81, A75, A82, AFF_1:21;
then b9,a9 // b9,p by AFF_1:def 1;
then p,b9 // a9,b9 by AFF_1:4;
then A109: p,b9 // a,b by A19, A30, AFF_1:5;
LIN o,a,a9 by A3, A8, A9, A14, AFF_1:21;
then o,a // o,a9 by AFF_1:def 1;
then A110: a,o // a9,o by AFF_1:4;
LIN q,r,b9 by A106, AFF_1:6;
then q,r // q,b9 by AFF_1:def 1;
then r,q // b9,q by AFF_1:4;
then r,q // a9,o by A101, A97, AFF_1:5;
then A111: a,o // r,q by A84, A110, AFF_1:5;
LIN r,b9,q by A106, AFF_1:6;
then r,b9 // r,q by AFF_1:def 1;
then a,o // r,b9 by A111, A107, AFF_1:4, AFF_1:5;
then A112: p,o // r,b by A2, A4, A10, A11, A15, A99, A102, A105, A109;
p,q // a,c by A20, A34, A100, AFF_1:5;
then A113: p,o // r,c by A2, A5, A12, A16, A92, A99, A102, A105, A111;
then r,c // r,b by A86, A112, AFF_1:5;
then LIN r,c,b by AFF_1:def 1;
then LIN c,b,r by AFF_1:6;
then c,b // c,r by AFF_1:def 1;
then A114: b,c // r,c by AFF_1:4;
b9,c9 // r,c by A86, A94, A113, AFF_1:5;
then r = c by A21, A114, AFF_1:5;
then b,c // p,o by A112, AFF_1:4;
hence contradiction by A21, A86, A94, AFF_1:5; :: thesis: verum