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

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

hence
Lambda OAP is Desarguesian
by AFF_2:def 4; :: thesis: verum
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 )

then A31: o1,c1,c19 are_collinear by Th2;

A32: ( a1,b1 '||' a19,b19 & a1,c1 '||' a19,c19 ) by A20, DIRAF:38;

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;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

hence contradiction by A27, A23, Th2; :: thesis: verum

end;

LIN o,c,c9
by A5, A13, A14, A17, AFF_1:21;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;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

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

assume
( o1,a1,b1 are_collinear or o1,a1,c1 are_collinear )
; :: thesis: contradictionassume
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;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

hence contradiction by A27, A23, Th2; :: thesis: verum

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;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

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

LIN o,a,a9
by A3, A9, A10, A15, AFF_1:21;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;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

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