let AP be AffinPlane; :: thesis: ( AP is satisfying_DES1_2 implies AP is Desarguesian )
assume A1: AP is satisfying_DES1_2 ; :: thesis: AP is Desarguesian
let A be Subset of AP; :: according to AFF_2:def 4 :: thesis: for b1, b2 being M3(K24( the U1 of AP))
for b3, b4, b5, b6, b7, b8, b9 being M3( the U1 of AP) holds
( not b3 in A or not b3 in b1 or not b3 in b2 or b3 = b4 or b3 = b5 or b3 = b6 or not b4 in A or not b7 in A or not b5 in b1 or not b8 in b1 or not b6 in b2 or not b9 in b2 or not A is being_line or not b1 is being_line or not b2 is being_line or A = b1 or A = b2 or not b4,b5 // b7,b8 or not b4,b6 // b7,b9 or b5,b6 // b8,b9 )
let P, C be Subset of AP; :: thesis: for b1, b2, b3, b4, b5, b6, b7 being M3( the U1 of AP) holds
( not b1 in A or not b1 in P or not b1 in C or b1 = b2 or b1 = b3 or b1 = b4 or not b2 in A or not b5 in A or not b3 in P or not b6 in P or not b4 in C or not b7 in C or not A is being_line or not P is being_line or not C is being_line or A = P or A = C or not b2,b3 // b5,b6 or not b2,b4 // b5,b7 or b3,b4 // b6,b7 )
let o, a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( not o in A or not o in P or not o in C or o = a or o = b or o = c or not a in A or not a9 in A or not b in P or not b9 in P or not c in C or not c9 in C or not A is being_line or not P is being_line or not C is being_line or A = P or A = C or not a,b // a9,b9 or not a,c // a9,c9 or b,c // b9,c9 )
assume that
A2: o in A and
A3: o in P and
A4: o in C and
A5: o <> a and
A6: o <> b and
A7: 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
now :: thesis: ( P <> C implies b,c // b9,c9 )
A21: ( not LIN o,b,a & not LIN o,a,c )
proof
A22: now :: thesis: not LIN o,a,c
assume LIN o,a,c ; :: thesis: contradiction
then c in A by A2, A5, A8, A14, AFF_1:25;
hence contradiction by A2, A4, A7, A12, A14, A16, A18, AFF_1:18; :: thesis: verum
end;
A23: now :: thesis: not LIN o,b,a
assume LIN o,b,a ; :: thesis: contradiction
then a in P by A3, A6, A10, A15, AFF_1:25;
hence contradiction by A2, A3, A5, A8, A14, A15, A17, AFF_1:18; :: thesis: verum
end;
assume ( LIN o,b,a or LIN o,a,c ) ; :: thesis: contradiction
hence contradiction by A23, A22; :: thesis: verum
end;
A24: ( b = b9 implies b,c // b9,c9 )
proof
A25: LIN o,c,c9 by A4, A12, A13, A16, AFF_1:21;
A26: LIN o,a,a9 by A2, A8, A9, A14, AFF_1:21;
assume A27: b = b9 ; :: thesis: b,c // b9,c9
then b,a // b,a9 by A19, AFF_1:4;
then a,c // a,c9 by A20, A21, A26, AFF_1:14;
then c = c9 by A21, A25, AFF_1:14;
hence b,c // b9,c9 by A27, AFF_1:2; :: thesis: verum
end;
A28: ( a9 = o implies b,c // b9,c9 )
proof
assume A29: a9 = o ; :: thesis: b,c // b9,c9
( LIN o,b,b9 & not LIN o,a,b ) by A3, A10, A11, A15, A21, AFF_1:6, AFF_1:21;
then A30: o = b9 by A19, A29, AFF_1:55;
LIN o,c,c9 by A4, A12, A13, A16, AFF_1:21;
then o = c9 by A20, A21, A29, AFF_1:55;
hence b,c // b9,c9 by A30, AFF_1:3; :: thesis: verum
end;
A31: ( c9 = o implies b,c // b9,c9 )
proof
A32: c,a // c9,a9 by A20, AFF_1:4;
assume A33: c9 = o ; :: thesis: b,c // b9,c9
( LIN o,a,a9 & not LIN o,c,a ) by A2, A8, A9, A14, A21, AFF_1:6, AFF_1:21;
hence b,c // b9,c9 by A28, A33, A32, AFF_1:55; :: thesis: verum
end;
set K = Line (a,c);
A34: a in Line (a,c) by AFF_1:15;
A35: a <> c by A2, A4, A5, A8, A12, A14, A16, A18, AFF_1:18;
then A36: Line (a,c) is being_line by AFF_1:def 3;
A37: c in Line (a,c) by AFF_1:15;
A38: a <> b by A2, A3, A5, A8, A10, A14, A15, A17, AFF_1:18;
A39: ( LIN a,b,c implies b,c // b9,c9 )
proof
consider N being Subset of AP such that
A40: a9 in N and
A41: Line (a,c) // N by A36, AFF_1:49;
A42: N is being_line by A41, AFF_1:36;
a9,c9 // Line (a,c) by A20, A35, AFF_1:29, AFF_1:32;
then a9,c9 // N by A41, AFF_1:43;
then A43: c9 in N by A40, A42, AFF_1:23;
assume LIN a,b,c ; :: thesis: b,c // b9,c9
then LIN a,c,b by AFF_1:6;
then A44: b in Line (a,c) by AFF_1:def 2;
then Line (a,c) = Line (a,b) by A38, A36, A34, AFF_1:57;
then a9,b9 // Line (a,c) by A19, A38, AFF_1:29, AFF_1:32;
then a9,b9 // N by A41, AFF_1:43;
then b9 in N by A40, A42, AFF_1:23;
hence b,c // b9,c9 by A37, A44, A41, A43, AFF_1:39; :: thesis: verum
end;
assume A45: P <> C ; :: thesis: b,c // b9,c9
A46: now :: thesis: ( o <> a9 & o <> b9 & o <> c9 & b <> b9 & not LIN a,b,c implies b,c // b9,c9 )
set T = Line (b9,a9);
set D = Line (b,a);
set N = Line (a9,c9);
assume that
A47: o <> a9 and
A48: o <> b9 and
A49: o <> c9 and
A50: b <> b9 and
A51: not LIN a,b,c ; :: thesis: b,c // b9,c9
A52: c9 in Line (a9,c9) by AFF_1:15;
assume not b,c // b9,c9 ; :: thesis: contradiction
then consider q being Element of AP such that
A53: LIN b,c,q and
A54: LIN b9,c9,q by AFF_1:60;
consider M being Subset of AP such that
A55: q in M and
A56: Line (a,c) // M by A36, AFF_1:49;
A57: M is being_line by A56, AFF_1:36;
not a,b // M then consider p being Element of AP such that
A58: p in M and
A59: LIN a,b,p by A57, AFF_1:59;
A60: a9 in Line (a9,c9) by AFF_1:15;
A61: p <> q
proof
A62: ( LIN p,b,a & LIN p,b,b ) by A59, AFF_1:6, AFF_1:7;
assume A63: p = q ; :: thesis: contradiction
then LIN p,b,c by A53, AFF_1:6;
then p = b by A51, A62, AFF_1:8;
then LIN b,b9,c9 by A54, A63, AFF_1:6;
then c9 in P by A10, A11, A15, A50, AFF_1:25;
hence contradiction by A3, A4, A13, A15, A16, A45, A49, AFF_1:18; :: thesis: verum
end;
A64: c,a // q,p by A34, A37, A55, A56, A58, AFF_1:39;
A65: LIN b,a,p by A59, AFF_1:6;
A66: b9 <> c9 by A3, A4, A11, A13, A15, A16, A45, A48, AFF_1:18;
A67: a9 <> c9 by A2, A4, A9, A13, A14, A16, A18, A47, AFF_1:18;
then A68: Line (a9,c9) is being_line by AFF_1:def 3;
A69: Line (a,c) // Line (a9,c9) by A20, A35, A67, AFF_1:37;
then A70: Line (a9,c9) // M by A56, AFF_1:44;
A71: a9 <> b9 by A2, A3, A9, A11, A14, A15, A17, A47, AFF_1:18;
A72: not LIN a9,b9,c9
proof
assume LIN a9,b9,c9 ; :: thesis: contradiction
then LIN a9,c9,b9 by AFF_1:6;
then b9 in Line (a9,c9) by AFF_1:def 2;
then a9,b9 // Line (a9,c9) by A68, A60, AFF_1:23;
then A73: a9,b9 // Line (a,c) by A69, AFF_1:43;
a9,b9 // a,b by A19, AFF_1:4;
then a,b // Line (a,c) by A71, A73, AFF_1:32;
then b in Line (a,c) by A36, A34, AFF_1:23;
hence contradiction by A36, A34, A37, A51, AFF_1:21; :: thesis: verum
end;
not b9,p // Line (a9,c9)
proof
assume b9,p // Line (a9,c9) ; :: thesis: contradiction
then b9,p // M by A70, AFF_1:43;
then p,b9 // M by AFF_1:34;
then A74: b9 in M by A57, A58, AFF_1:23;
A75: now :: thesis: not b9 <> q
assume A76: b9 <> q ; :: thesis: contradiction
LIN b9,q,c9 by A54, AFF_1:6;
then c9 in M by A55, A57, A74, A76, AFF_1:25;
then ( a9 in Line (a9,c9) & b9 in Line (a9,c9) ) by A52, A70, A74, AFF_1:15, AFF_1:45;
hence contradiction by A68, A52, A72, AFF_1:21; :: thesis: verum
end;
now :: thesis: not b9 = q
assume b9 = q ; :: thesis: contradiction
then LIN b,b9,c by A53, AFF_1:6;
then c in P by A10, A11, A15, A50, AFF_1:25;
hence contradiction by A3, A4, A7, A12, A15, A16, A45, AFF_1:18; :: thesis: verum
end;
hence contradiction by A75; :: thesis: verum
end;
then consider x being Element of AP such that
A77: x in Line (a9,c9) and
A78: LIN b9,p,x by A68, AFF_1:59;
set A9 = Line (x,a);
A79: a <> a9
proof
assume A80: a = a9 ; :: thesis: contradiction
( not LIN o,a,b & LIN o,b,b9 ) by A3, A10, A11, A15, A21, AFF_1:6, AFF_1:21;
hence contradiction by A19, A50, A80, AFF_1:14; :: thesis: verum
end;
A81: x <> a
proof
assume x = a ; :: thesis: contradiction
then a9 in Line (a,c) by A34, A60, A69, A77, AFF_1:45;
then A = Line (a,c) by A8, A9, A14, A36, A34, A79, AFF_1:18;
hence contradiction by A2, A4, A7, A12, A14, A16, A18, A37, AFF_1:18; :: thesis: verum
end;
then A82: Line (x,a) is being_line by AFF_1:def 3;
A83: c <> c9
proof
assume c = c9 ; :: thesis: contradiction
then A84: c,a // c,a9 by A20, AFF_1:4;
( not LIN o,c,a & LIN o,a,a9 ) by A2, A8, A9, A14, A21, AFF_1:6, AFF_1:21;
hence contradiction by A79, A84, AFF_1:14; :: thesis: verum
end;
A85: not LIN b9,c9,x
proof
A86: now :: thesis: ( c9 = x implies LIN b9,c9,a9 )
A87: now :: thesis: not q = c9
assume q = c9 ; :: thesis: contradiction
then LIN c,c9,b by A53, AFF_1:6;
then b in C by A12, A13, A16, A83, AFF_1:25;
hence contradiction by A3, A4, A6, A10, A15, A16, A45, AFF_1:18; :: thesis: verum
end;
assume c9 = x ; :: thesis: LIN b9,c9,a9
then A88: LIN b9,c9,p by A78, AFF_1:6;
LIN b9,c9,c9 by AFF_1:7;
then c9 in M by A66, A54, A55, A57, A58, A61, A88, AFF_1:8, AFF_1:25;
then A89: q in Line (a9,c9) by A55, A52, A70, AFF_1:45;
LIN q,c9,b9 by A54, AFF_1:6;
then ( q = c9 or b9 in Line (a9,c9) ) by A68, A52, A89, AFF_1:25;
hence LIN b9,c9,a9 by A68, A60, A52, A87, AFF_1:21; :: thesis: verum
end;
assume LIN b9,c9,x ; :: thesis: contradiction
then A90: LIN c9,x,b9 by AFF_1:6;
A91: ( LIN c9,x,a9 & LIN c9,x,c9 ) by A68, A60, A52, A77, AFF_1:21;
then LIN c9,a9,b9 by A90, A86, AFF_1:6, AFF_1:8;
then c9,a9 // c9,b9 by AFF_1:def 1;
then a9,c9 // b9,c9 by AFF_1:4;
then A92: a,c // b9,c9 by A20, A67, AFF_1:5;
( c9 = x or LIN b9,c9,a9 ) by A90, A91, AFF_1:8;
then b9,c9 // b9,a9 by A86, AFF_1:def 1;
then b9,c9 // a9,b9 by AFF_1:4;
then b9,c9 // a,b by A19, A71, AFF_1:5;
then a,c // a,b by A66, A92, AFF_1:5;
then LIN a,c,b by AFF_1:def 1;
hence contradiction by A51, AFF_1:6; :: thesis: verum
end;
A93: ( x in Line (x,a) & a in Line (x,a) ) by AFF_1:15;
A <> Line (a,c) by A2, A4, A7, A12, A14, A16, A18, A37, AFF_1:18;
then A94: A <> Line (a9,c9) by A8, A34, A69, AFF_1:45;
A95: not LIN b,c,a by A51, AFF_1:6;
A96: p in Line (b,a) by A59, AFF_1:def 2;
A97: ( Line (b,a) is being_line & b in Line (b,a) ) by A38, AFF_1:15, AFF_1:def 3;
A98: LIN b9,x,p by A78, AFF_1:6;
c,a // c9,x by A34, A37, A52, A69, A77, AFF_1:39;
then o in Line (x,a) by A1, A3, A4, A6, A7, A10, A11, A12, A13, A15, A16, A45, A53, A54, A98, A81, A82, A93, A61, A85, A64, A95, A65;
then x in A by A2, A5, A8, A14, A82, A93, AFF_1:18;
then x = a9 by A9, A14, A68, A60, A77, A94, AFF_1:18;
then A99: ( a9 in Line (b9,a9) & p in Line (b9,a9) ) by A98, AFF_1:15, AFF_1:def 2;
Line (b,a) // Line (b9,a9) by A19, A38, A71, AFF_1:37;
then ( a in Line (b,a) & a9 in Line (b,a) ) by A96, A99, AFF_1:15, AFF_1:45;
then b in A by A8, A9, A14, A79, A97, AFF_1:18;
hence contradiction by A2, A3, A6, A10, A14, A15, A17, AFF_1:18; :: thesis: verum
end;
( b9 = o implies b,c // b9,c9 )
proof
assume A100: b9 = o ; :: thesis: b,c // b9,c9
( LIN o,a,a9 & b,a // b9,a9 ) by A2, A8, A9, A14, A19, AFF_1:4, AFF_1:21;
hence b,c // b9,c9 by A21, A28, A100, AFF_1:55; :: thesis: verum
end;
hence b,c // b9,c9 by A28, A31, A39, A24, A46; :: thesis: verum
end;
hence b,c // b9,c9 by A10, A11, A12, A13, A15, AFF_1:51; :: thesis: verum