let AP be AffinPlane; :: thesis: ( AP is Desarguesian implies AP is satisfying_DES1_2 )
assume A1: AP is Desarguesian ; :: thesis: AP is satisfying_DES1_2
then A2: AP is satisfying_DES_1 by AFF_2:2;
let A be Subset of AP; :: according to AFF_3:def 3 :: thesis: for P, C being Subset of AP
for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
o in C
let P, C be Subset of AP; :: thesis: for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
o in C
let o, a, a9, b, b9, c, c9, p, q be Element of AP; :: thesis: ( A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q implies o in C )
assume that
A3: A is being_line and
A4: P is being_line and
A5: C is being_line and
A6: P <> A and
A7: P <> C and
A <> C and
A8: o in A and
A9: ( a in A & a9 in A ) and
A10: o in P and
A11: b in P and
A12: b9 in P and
A13: c in C and
A14: c9 in C and
A15: o <> a and
A16: o <> b and
o <> c and
A17: p <> q and
A18: not LIN b,a,c and
A19: not LIN b9,a9,c9 and
A20: c <> c9 and
A21: LIN b,a,p and
A22: LIN b9,a9,p and
A23: LIN b,c,q and
A24: LIN b9,c9,q and
A25: a,c // a9,c9 and
A26: a,c // p,q ; :: thesis: o in C
A27: b <> p by A17, A18, A23, A26, AFF_1:55;
set K = Line (b9,a9);
A28: p in Line (b9,a9) by A22, AFF_1:def 2;
a9 <> b9 by A19, AFF_1:7;
then A29: Line (b9,a9) is being_line by AFF_1:def 3;
A30: b <> q
proof
assume A31: b = q ; :: thesis: contradiction
( not LIN b,c,a & c,a // q,p ) by A18, A26, AFF_1:4, AFF_1:6;
hence contradiction by A17, A21, A31, AFF_1:55; :: thesis: verum
end;
set M = Line (b9,c9);
A32: q in Line (b9,c9) by A24, AFF_1:def 2;
A33: c9 in Line (b9,c9) by AFF_1:15;
A34: a <> c by A18, AFF_1:7;
A35: b9 <> p
proof
assume A36: b9 = p ; :: thesis: contradiction
a9,c9 // p,q by A25, A26, A34, AFF_1:5;
hence contradiction by A17, A19, A24, A36, AFF_1:55; :: thesis: verum
end;
A37: b9 <> q
proof
a9,c9 // p,q by A25, A26, A34, AFF_1:5;
then A38: c9,a9 // q,p by AFF_1:4;
assume A39: b9 = q ; :: thesis: contradiction
not LIN b9,c9,a9 by A19, AFF_1:6;
hence contradiction by A17, A22, A39, A38, AFF_1:55; :: thesis: verum
end;
A40: b <> c by A18, AFF_1:7;
A41: a <> b by A18, AFF_1:7;
A42: ( b9 <> a9 & b9 <> c9 ) by A19, AFF_1:7;
A43: a9 in Line (b9,a9) by AFF_1:15;
A44: b9 in Line (b9,c9) by AFF_1:15;
A45: b9 <> c9 by A19, AFF_1:7;
then A46: Line (b9,c9) is being_line by AFF_1:def 3;
A47: b9 in Line (b9,a9) by AFF_1:15;
then A48: Line (b9,a9) <> Line (b9,c9) by A19, A29, A43, A33, AFF_1:21;
now :: thesis: o in C
A49: now :: thesis: ( Line (b9,c9) <> P implies o in C )
p,q // a9,c9 by A25, A26, A34, AFF_1:5;
then A50: c9,a9 // q,p by AFF_1:4;
A51: b,a // b,p by A21, AFF_1:def 1;
set D = Line (b,c);
A52: b in Line (b,c) by AFF_1:15;
Line (b,c) is being_line by A40, AFF_1:def 3;
then consider D9 being Subset of AP such that
A53: c9 in D9 and
A54: Line (b,c) // D9 by AFF_1:49;
A55: D9 is being_line by A54, AFF_1:36;
A56: q in Line (b,c) by A23, AFF_1:def 2;
assume A57: Line (b9,c9) <> P ; :: thesis: o in C
not D9 // P
proof
assume D9 // P ; :: thesis: contradiction
then Line (b,c) // P by A54, AFF_1:44;
then q in P by A11, A52, A56, AFF_1:45;
hence contradiction by A4, A12, A46, A44, A32, A37, A57, AFF_1:18; :: thesis: verum
end;
then consider d being Element of AP such that
A58: d in D9 and
A59: d in P by A4, A55, AFF_1:58;
A60: c in Line (b,c) by AFF_1:15;
A61: d <> b9
proof
assume d = b9 ; :: thesis: contradiction
then Line (b9,c9) = D9 by A45, A46, A44, A33, A53, A55, A58, AFF_1:18;
then A62: Line (b,c) = Line (b9,c9) by A32, A56, A54, AFF_1:45;
then LIN c,c9,b by A46, A33, A52, A60, AFF_1:21;
then A63: b in C by A5, A13, A14, A20, AFF_1:25;
set N = Line (a,c);
set T = Line (b,a);
A64: b in Line (b,a) by AFF_1:15;
A65: c in Line (a,c) by AFF_1:15;
A66: a in Line (b,a) by AFF_1:15;
A67: Line (a,c) is being_line by A34, AFF_1:def 3;
A68: a in Line (a,c) by AFF_1:15;
A69: a <> a9
proof
assume a = a9 ; :: thesis: contradiction
then LIN a,c,c9 by A25, AFF_1:def 1;
then c9 in Line (a,c) by AFF_1:def 2;
then Line (a,c) = C by A5, A13, A14, A20, A67, A65, AFF_1:18;
hence contradiction by A13, A18, A63, A67, A68, AFF_1:21; :: thesis: verum
end;
A70: ( Line (b,a) is being_line & p in Line (b,a) ) by A21, A41, AFF_1:def 2, AFF_1:def 3;
A71: b <> b9
proof
A72: Line (b9,a9) <> Line (b,a)
proof
assume Line (b9,a9) = Line (b,a) ; :: thesis: contradiction
then Line (b,a) = A by A3, A9, A29, A43, A66, A69, AFF_1:18;
hence contradiction by A3, A4, A6, A8, A10, A11, A16, A64, AFF_1:18; :: thesis: verum
end;
assume b = b9 ; :: thesis: contradiction
hence contradiction by A29, A47, A28, A35, A64, A70, A72, AFF_1:18; :: thesis: verum
end;
LIN c,c9,b9 by A46, A44, A33, A60, A62, AFF_1:21;
then b9 in C by A5, A13, A14, A20, AFF_1:25;
hence contradiction by A4, A5, A7, A11, A12, A63, A71, AFF_1:18; :: thesis: verum
end;
c9,d // q,b by A52, A56, A53, A54, A58, AFF_1:39;
then d,a9 // b,p by A1, A4, A11, A12, A42, A29, A46, A47, A43, A28, A44, A33, A32, A48, A57, A59, A61, A50;
then A73: b,a // d,a9 by A27, A51, AFF_1:5;
b,c // d,c9 by A52, A60, A53, A54, A58, AFF_1:39;
hence o in C by A2, A3, A4, A5, A6, A8, A9, A10, A11, A13, A14, A15, A16, A18, A20, A25, A59, A73; :: thesis: verum
end;
now :: thesis: ( Line (b9,c9) = P implies o in C )
assume A74: Line (b9,c9) = P ; :: thesis: o in C
LIN b,q,c by A23, AFF_1:6;
then c in P by A11, A46, A32, A30, A74, AFF_1:25;
then P = Line (c,c9) by A20, A46, A33, A74, AFF_1:57;
hence o in C by A5, A10, A13, A14, A20, AFF_1:57; :: thesis: verum
end;
hence o in C by A49; :: thesis: verum
end;
hence o in C ; :: thesis: verum