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:16;
let A be Subset of AP; :: according to AFF_3:def 3 :: thesis: for P, C being Subset of AP
for o, a, a', b, b', c, c', 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 & a' in A & o in P & b in P & b' in P & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b',a',c' & c <> c' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q holds
o in C
let P, C be Subset of AP; :: thesis: for o, a, a', b, b', c, c', 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 & a' in A & o in P & b in P & b' in P & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b',a',c' & c <> c' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q holds
o in C
let o, a, a', b, b', c, c', 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 & a' in A & o in P & b in P & b' in P & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b',a',c' & c <> c' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q implies o in C )
assume that
A3: ( A is being_line & P is being_line & C is being_line ) and
A4: ( P <> A & P <> C & A <> C ) and
A5: ( o in A & a in A & a' in A & o in P & b in P & b' in P & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b',a',c' & c <> c' ) and
A6: ( LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q ) ; :: thesis: o in C
A7: ( a <> b & a <> c & b <> c & a' <> b' & a' <> c' & b' <> c' ) by A5, AFF_1:16;
A8: ( b' <> a' & b' <> c' ) by A5, AFF_1:16;
set K = Line b',a';
set M = Line b',c';
A9: ( Line b',a' is being_line & Line b',c' is being_line & b' in Line b',a' & a' in Line b',a' & p in Line b',a' & b' in Line b',c' & c' in Line b',c' & q in Line b',c' ) by A6, A7, AFF_1:26, AFF_1:def 2, AFF_1:def 3;
then A10: Line b',a' <> Line b',c' by A5, AFF_1:33;
A11: b <> q

proof

assume A12: b = q ; :: thesis: contradiction
( not LIN b,c,a & c,a // q,p ) by A5, A6, AFF_1:13, AFF_1:15;
hence contradiction by A5, A6, A12, AFF_1:69; :: thesis: verum

end;

A13: b' <> q

proof

assume A14: b' = q ; :: thesis: contradiction
a',c' // p,q by A6, A7, AFF_1:14;
then ( c',a' // q,p & not LIN b',c',a' ) by A5, AFF_1:13, AFF_1:15;
hence contradiction by A5, A6, A14, AFF_1:69; :: thesis: verum

end;

A15: b' <> p

proof

assume A16: b' = p ; :: thesis: contradiction
a',c' // p,q by A6, A7, AFF_1:14;
hence contradiction by A5, A6, A16, AFF_1:69; :: thesis: verum

end;

A17: b <> p by A5, A6, AFF_1:69;

now

A18: now

assume A19: Line b',c' = P ; :: thesis: o in C
LIN b,q,c by A6, AFF_1:15;
then c in P by A5, A9, A11, A19, AFF_1:39;
then P = Line c,c' by A5, A9, A19, AFF_1:71;
hence o in C by A3, A5, AFF_1:71; :: thesis: verum

end;

now

assume A20: Line b',c' <> P ; :: thesis: o in C
set D = Line b,c;
A21: ( Line b,c is being_line & b in Line b,c & c in Line b,c & q in Line b,c ) by A6, A7, AFF_1:26, AFF_1:def 2, AFF_1:def 3;
then consider D' being Subset of AP such that
A22: ( c' in D' & Line b,c // D' ) by AFF_1:63;
A23: D' is being_line by A22, AFF_1:50;
not D' // P

proof

assume D' // P ; :: thesis: contradiction
then Line b,c // P by A22, AFF_1:58;
then q in P by A5, A21, AFF_1:59;
hence contradiction by A3, A5, A9, A13, A20, AFF_1:30; :: thesis: verum

end;

then consider d being Element of AP such that
A24: ( d in D' & d in P ) by A3, A23, AFF_1:72;
A25: ( q,b // c',d & b,c // d,c' ) by A21, A22, A24, AFF_1:53;
A26: ( c',d // q,b & b,c // d,c' ) by A21, A22, A24, AFF_1:53;
A27: d <> b'

proof

assume d = b' ; :: thesis: contradiction
then Line b',c' = D' by A7, A9, A22, A23, A24, AFF_1:30;
then Line b,c = Line b',c' by A9, A21, A22, AFF_1:59;
then ( LIN c,c',b & LIN c,c',b' ) by A9, A21, AFF_1:33;
then A28: ( b in C & b' in C ) by A3, A5, AFF_1:39;
set T = Line b,a;
set N = Line a,c;
A29: ( Line b,a is being_line & b in Line b,a & a in Line b,a & p in Line b,a ) by A6, A7, AFF_1:26, AFF_1:def 2, AFF_1:def 3;
A30: ( Line a,c is being_line & a in Line a,c & c in Line a,c ) by A7, AFF_1:26, AFF_1:def 3;
A31: a <> a'

proof

assume a = a' ; :: thesis: contradiction
then LIN a,c,c' by A6, AFF_1:def 1;
then c' in Line a,c by AFF_1:def 2;
then Line a,c = C by A3, A5, A30, AFF_1:30;
hence contradiction by A5, A28, A30, AFF_1:33; :: thesis: verum

end;

b <> b'

proof

assume A32: b = b' ; :: thesis: contradiction
Line b',a' <> Line b,a

proof

assume Line b',a' = Line b,a ; :: thesis: contradiction
then Line b,a = A by A3, A5, A9, A29, A31, AFF_1:30;
hence contradiction by A3, A4, A5, A29, AFF_1:30; :: thesis: verum

end;

hence contradiction by A9, A15, A29, A32, AFF_1:30; :: thesis: verum

end;

hence contradiction by A3, A4, A5, A28, AFF_1:30; :: thesis: verum

end;

p,q // a',c' by A6, A7, AFF_1:14;
then c',a' // q,p by AFF_1:13;
then A33: d,a' // b,p by A1, A3, A5, A8, A9, A10, A20, A24, A26, A27, AFF_2:def 4;
b,a // b,p by A6, AFF_1:def 1;
then b,a // d,a' by A17, A33, AFF_1:14;
hence o in C by A2, A3, A4, A5, A6, A24, A25, AFF_2:def 5; :: thesis: verum

end;

hence o in C by A18; :: thesis: verum

end;

hence o in C ; :: thesis: verum