let OAP be OAffinSpace; :: thesis: ( OAP is satisfying_DES_1 implies Lambda OAP is Desarguesian )
assume A1: OAP is satisfying_DES_1 ; :: thesis: Lambda OAP is Desarguesian
then A2: OAP is satisfying_DES by Th11;
set AP = Lambda OAP;
for A, P, C being Subset of (Lambda OAP)
for o, a, b, c, a', b', c' being Element of (Lambda OAP) st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'

proof

let A, P, C be Subset of (Lambda OAP); :: thesis: for o, a, b, c, a', b', c' being Element of (Lambda OAP) st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
let o, a, b, c, a', b', c' be Element of (Lambda OAP); :: thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' implies b,c // b',c' )
assume that
A3: ( o in A & o in P & o in C ) and
A4: ( o <> a & o <> b & o <> c ) and
A5: ( a in A & a' in A & b in P & b' in P & c in C & c' in C ) and
A6: ( A is being_line & P is being_line & C is being_line ) and
A7: ( A <> P & A <> C ) and
A8: ( a,b // a',b' & a,c // a',c' ) ; :: thesis: b,c // b',c'
reconsider o1 = o, a1 = a, b1 = b, c1 = c, a1' = a', b1' = b', c1' = c' as Element of OAP by Th2;
A9: ( LIN o1,a1,a1' & LIN o1,b1,b1' & LIN o1,c1,c1' )

proof

( LIN o,a,a' & LIN o,b,b' & LIN o,c,c' ) by A3, A5, A6, AFF_1:33;
hence ( LIN o1,a1,a1' & LIN o1,b1,b1' & LIN o1,c1,c1' ) by Th3; :: thesis: verum

end;

A10: ( not LIN o1,a1,b1 & not LIN o1,a1,c1 )

proof

assume A11: ( LIN o1,a1,b1 or LIN o1,a1,c1 ) ; :: thesis: contradiction

A12: now

assume LIN o,a,b ; :: thesis: contradiction
then consider X being Subset of (Lambda OAP) such that
A13: ( X is being_line & o in X & a in X & b in X ) by AFF_1:33;
( X = P & X = A ) by A3, A4, A5, A6, A13, AFF_1:30;
hence contradiction by A7; :: thesis: verum

end;

now

assume LIN o,a,c ; :: thesis: contradiction
then consider X being Subset of (Lambda OAP) such that
A14: ( X is being_line & o in X & a in X & c in X ) by AFF_1:33;
( X = C & X = A ) by A3, A4, A5, A6, A14, AFF_1:30;
hence contradiction by A7; :: thesis: verum

end;

hence contradiction by A11, A12, Th3; :: thesis: verum

end;

A15: ( a1,o1 // o1,a1' or o1,a1 // o1,a1' )

proof

( Mid o1,a1,a1' or Mid a1,o1,a1' or Mid o1,a1',a1 ) by A9, DIRAF:35;
hence ( a1,o1 // o1,a1' or o1,a1 // o1,a1' ) by DIRAF:11, DIRAF:def 3; :: thesis: verum

end;

A16: ( a1,b1 '||' a1',b1' & a1,c1 '||' a1',c1' ) by A8, DIRAF:45;

A17: now

assume A18: a1,o1 // o1,a1' ; :: thesis: b,c // b',c'
then ( b1,o1 // o1,b1' & c1,o1 // o1,c1' & a1,b1 // b1',a1' & a1,c1 // c1',a1' ) by A9, A10, A16, Th12;
then b1,c1 // c1',b1' by A1, A10, A18, Def16;
then b1,c1 '||' b1',c1' by DIRAF:def 4;
hence b,c // b',c' by DIRAF:45; :: thesis: verum

end;

now

assume A19: o1,a1 // o1,a1' ; :: thesis: b,c // b',c'
then ( o1,b1 // o1,b1' & o1,c1 // o1,c1' & a1,b1 // a1',b1' & a1,c1 // a1',c1' ) by A9, A10, A16, Th13;
then b1,c1 // b1',c1' by A2, A10, A19, Def15;
then b1,c1 '||' b1',c1' by DIRAF:def 4;
hence b,c // b',c' by DIRAF:45; :: thesis: verum

end;

hence b,c // b',c' by A15, A17; :: thesis: verum

end;

hence Lambda OAP is Desarguesian by AFF_2:def 4; :: thesis: verum