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

proof

let A, P, C be Subset of (Lambda OAP); :: thesis: for o, a, b, c, a9, b9, c9 being Element of (Lambda OAP) st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let o, a, b, c, a9, b9, c9 be Element of (Lambda OAP); :: thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
reconsider o1 = o, a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of OAP by Th1;
assume that
A3: o in A and
A4: o in P and
A5: o in C and
A6: o <> a and
A7: o <> b and
A8: o <> c and
A9: a in A and
A10: a9 in A and
A11: b in P and
A12: b9 in P and
A13: c in C and
A14: c9 in C and
A15: A is being_line and
A16: P is being_line and
A17: C is being_line and
A18: A <> P and
A19: A <> C and
A20: ( a,b // a9,b9 & a,c // a9,c9 ) ; :: thesis: b,c // b9,c9
LIN o,b,b9 by A4, A11, A12, A16, AFF_1:21;
then A21: o1,b1,b19 are_collinear by Th2;
A22: ( not o1,a1,b1 are_collinear & not o1,a1,c1 are_collinear )

proof

A23: now :: thesis: not LIN o,a,c

assume LIN o,a,c ; :: thesis: contradiction
then consider X being Subset of (Lambda OAP) such that
A24: ( X is being_line & o in X ) and
A25: a in X and
A26: c in X by AFF_1:21;
X = C by A5, A8, A13, A17, A24, A26, AFF_1:18;
hence contradiction by A3, A6, A9, A15, A19, A24, A25, AFF_1:18; :: thesis: verum

end;

A27: now :: thesis: not LIN o,a,b

assume LIN o,a,b ; :: thesis: contradiction
then consider X being Subset of (Lambda OAP) such that
A28: ( X is being_line & o in X ) and
A29: a in X and
A30: b in X by AFF_1:21;
X = P by A4, A7, A11, A16, A28, A30, AFF_1:18;
hence contradiction by A3, A6, A9, A15, A18, A28, A29, AFF_1:18; :: thesis: verum

end;

assume ( o1,a1,b1 are_collinear or o1,a1,c1 are_collinear ) ; :: thesis: contradiction
hence contradiction by A27, A23, Th2; :: thesis: verum

end;

LIN o,c,c9 by A5, A13, A14, A17, AFF_1:21;
then A31: o1,c1,c19 are_collinear by Th2;
A32: ( a1,b1 '||' a19,b19 & a1,c1 '||' a19,c19 ) by A20, DIRAF:38;

A33: now :: thesis: ( a1,o1 // o1,a19 implies b,c // b9,c9 )

assume A34: a1,o1 // o1,a19 ; :: thesis: b,c // b9,c9
then A35: ( a1,b1 // b19,a19 & a1,c1 // c19,a19 ) by A21, A31, A22, A32, Th7;
( b1,o1 // o1,b19 & c1,o1 // o1,c19 ) by A21, A31, A22, A32, A34, Th7;
then b1,c1 // c19,b19 by A1, A22, A34, A35;
then b1,c1 '||' b19,c19 by DIRAF:def 4;
hence b,c // b9,c9 by DIRAF:38; :: thesis: verum

end;

A36: now :: thesis: ( o1,a1 // o1,a19 implies b,c // b9,c9 )

assume A37: o1,a1 // o1,a19 ; :: thesis: b,c // b9,c9
then A38: ( a1,b1 // a19,b19 & a1,c1 // a19,c19 ) by A21, A31, A22, A32, Th8;
( o1,b1 // o1,b19 & o1,c1 // o1,c19 ) by A21, A31, A22, A32, A37, Th8;
then b1,c1 // b19,c19 by A2, A22, A37, A38;
then b1,c1 '||' b19,c19 by DIRAF:def 4;
hence b,c // b9,c9 by DIRAF:38; :: thesis: verum

end;

LIN o,a,a9 by A3, A9, A10, A15, AFF_1:21;
then o1,a1,a19 are_collinear by Th2;
then ( Mid o1,a1,a19 or Mid a1,o1,a19 or Mid o1,a19,a1 ) by DIRAF:29;
hence b,c // b9,c9 by A33, A36, DIRAF:7, DIRAF:def 3; :: thesis: verum

end;

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