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

proof

assume LIN o,a,c ; :: thesis: contradiction
then c in A by A2, A4, AFF_1:39;
hence contradiction by A2, A3, A4, AFF_1:30; :: thesis: verum

end;

A9: o <> a'

proof

assume A10: o = a' ; :: thesis: contradiction
( LIN o,a,a' & LIN o,c,c' ) by A2, A4, AFF_1:33;
hence contradiction by A5, A6, A8, A10, AFF_1:69; :: thesis: verum

end;

A11: o <> c'

proof

assume A12: o = c' ; :: thesis: contradiction
( LIN o,a,a' & LIN o,c,c' & c,a // c',a' & not LIN o,c,a ) by A2, A4, A5, A8, AFF_1:13, AFF_1:15, AFF_1:33;
hence contradiction by A9, A12, AFF_1:69; :: thesis: verum

end;

A13: c <> c'

proof

assume c = c' ; :: thesis: contradiction
then ( LIN o,a,a' & c,a // c,a' & not LIN o,c,a ) by A2, A4, A5, A8, AFF_1:13, AFF_1:15, AFF_1:33;
hence contradiction by A4, AFF_1:23; :: thesis: verum

end;

A14: ( Line b',a' <> P & Line b',c' <> P & Line b',a' <> Line b',c' ) by A2, A3, A4, A7, A9, A11, AFF_1:30, AFF_1:33;
set D = Line b,c;
A15: ( Line b,c is being_line & b in Line b,c & c in Line b,c & q in Line b,c ) by A5, A6, AFF_1:26, AFF_1:def 2, AFF_1:def 3;
then consider D' being Subset of AP such that
A16: ( c' in D' & Line b,c // D' ) by AFF_1:63;
A17: ( D' is being_line & D' // Line b,c ) by A16, AFF_1:50;
not D' // P

proof

assume D' // P ; :: thesis: contradiction
then Line b,c // P by A16, AFF_1:58;
then c in P by A4, A15, AFF_1:59;
hence contradiction by A2, A3, A4, AFF_1:30; :: thesis: verum

end;

then consider d being Element of AP such that
A18: ( d in D' & d in P ) by A2, A17, AFF_1:72;
A19: d <> b'

proof

assume d = b' ; :: thesis: contradiction
then Line b',c' = D' by A6, A7, A16, A17, A18, AFF_1:30;
then Line b,c = Line b',c' by A7, A15, A16, AFF_1:59;
then LIN c,c',b by A7, A15, AFF_1:33;
then b in C by A2, A4, A13, AFF_1:39;
hence contradiction by A2, A3, A4, AFF_1:30; :: thesis: verum

end;

( c,b // c',d & c,a // c',a' ) by A5, A15, A16, A18, AFF_1:13, AFF_1:53;
then A20: b,a // d,a' by A1, A2, A3, A4, A18, AFF_2:def 4;
b,a // b,p by A5, AFF_1:def 1;
then ( d,a' // b,p & d,c' // b,q ) by A6, A15, A16, A18, A20, AFF_1:14, AFF_1:53;
then a',c' // p,q by A1, A2, A4, A6, A7, A14, A18, A19, AFF_2:def 4;
hence a,c // p,q by A5, A6, AFF_1:14; :: thesis: verum