let MS be OrtAfPl; :: thesis: ( MS is satisfying_DES iff AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian )
set AS = AffinStruct(# the carrier of MS, the CONGR of MS #);

A1: now :: thesis: ( MS is satisfying_DES implies AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian )

assume A2: MS is satisfying_DES ; :: thesis: AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian

now :: thesis: for A, P, C being Subset of AffinStruct(# the carrier of MS, the CONGR of MS #)
for o, a, b, c, a9, b9, c9 being Element of AffinStruct(# the carrier of MS, the CONGR of MS #) 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 A, P, C be Subset of AffinStruct(# the carrier of MS, the CONGR of MS #); :: thesis: for o, a, b, c, a9, b9, c9 being Element of AffinStruct(# the carrier of MS, the CONGR of MS #) 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 AffinStruct(# the carrier of MS, the CONGR of MS #); :: 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 )
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 and
A21: a,c // a9,c9 ; :: thesis: b,c // b9,c9

now :: thesis: ( o <> a9 & a <> a9 implies b,c // b9,c9 )

reconsider o1 = o, a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of MS ;
assume that
A22: o <> a9 and
A23: a <> a9 ; :: thesis: b,c // b9,c9
A24: ( a1,b1 // a19,b19 & a1,c1 // a19,c19 ) by A20, A21, ANALMETR:36;
A25: b <> b9 by A3, A4, A6, A7, A9, A10, A11, A15, A16, A18, A20, A23, AFF_4:9;

now :: thesis: not LIN b,b9,a

assume LIN b,b9,a ; :: thesis: contradiction
then a in P by A11, A12, A16, A25, AFF_1:25;
hence contradiction by A3, A4, A6, A9, A15, A16, A18, AFF_1:18; :: thesis: verum

end;

then A26: not LIN b1,b19,a1 by ANALMETR:40;
LIN o,a,a9 by A3, A9, A10, A15, AFF_1:21;
then A27: LIN o1,a1,a19 by ANALMETR:40;

now :: thesis: not LIN a,a9,c

assume LIN a,a9,c ; :: thesis: contradiction
then c in A by A9, A10, A15, A23, AFF_1:25;
hence contradiction by A3, A5, A8, A13, A15, A17, A19, AFF_1:18; :: thesis: verum

end;

then A28: not LIN a1,a19,c1 by ANALMETR:40;
LIN o,b,b9 by A4, A11, A12, A16, AFF_1:21;
then A29: LIN o1,b1,b19 by ANALMETR:40;
LIN o,c,c9 by A5, A13, A14, A17, AFF_1:21;
then A30: LIN o1,c1,c19 by ANALMETR:40;
( o1 <> b19 & o1 <> c19 ) by A3, A4, A5, A6, A7, A8, A9, A10, A11, A13, A15, A16, A17, A18, A19, A20, A21, A22, AFF_4:8;
then b1,c1 // b19,c19 by A2, A6, A7, A8, A22, A27, A29, A30, A24, A26, A28, CONAFFM:def 1;
hence b,c // b9,c9 by ANALMETR:36; :: thesis: verum

end;

hence b,c // b9,c9 by A3, A4, A5, A6, A7, A8, A9, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, AFPROJ:50; :: thesis: verum

end;

hence AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian by AFF_2:def 4; :: thesis: verum

end;

now :: thesis: ( AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian implies MS is satisfying_DES )

assume A31: AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian ; :: thesis: MS is satisfying_DES

now :: thesis: for o, a, a1, b, b1, c, c1 being Element of MS st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & not LIN b,b1,a & not LIN a,a1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1

let o, a, a1, b, b1, c, c1 be Element of MS; :: thesis: ( o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & not LIN b,b1,a & not LIN a,a1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,c // a1,c1 implies b,c // b1,c1 )
assume that
A32: o <> a and
o <> a1 and
A33: o <> b and
o <> b1 and
A34: o <> c and
o <> c1 and
A35: not LIN b,b1,a and
A36: not LIN a,a1,c and
A37: LIN o,a,a1 and
A38: LIN o,b,b1 and
A39: LIN o,c,c1 and
A40: ( a,b // a1,b1 & a,c // a1,c1 ) ; :: thesis: b,c // b1,c1
reconsider o9 = o, a9 = a, b9 = b, c9 = c, a19 = a1, b19 = b1, c19 = c1 as Element of AffinStruct(# the carrier of MS, the CONGR of MS #) ;
LIN o9,a9,a19 by A37, ANALMETR:40;
then consider A being Subset of AffinStruct(# the carrier of MS, the CONGR of MS #) such that
A41: A is being_line and
A42: o9 in A and
A43: a9 in A and
A44: a19 in A by AFF_1:21;
LIN o9,c9,c19 by A39, ANALMETR:40;
then consider C being Subset of AffinStruct(# the carrier of MS, the CONGR of MS #) such that
A45: ( C is being_line & o9 in C ) and
A46: c9 in C and
A47: c19 in C by AFF_1:21;
A48: A <> C

proof

assume A = C ; :: thesis: contradiction
then LIN a9,a19,c9 by A41, A43, A44, A46, AFF_1:21;
hence contradiction by A36, ANALMETR:40; :: thesis: verum

end;

LIN o9,b9,b19 by A38, ANALMETR:40;
then consider P being Subset of AffinStruct(# the carrier of MS, the CONGR of MS #) such that
A49: P is being_line and
A50: o9 in P and
A51: ( b9 in P & b19 in P ) by AFF_1:21;
A52: A <> P

proof

assume A = P ; :: thesis: contradiction
then LIN b9,b19,a9 by A43, A49, A51, AFF_1:21;
hence contradiction by A35, ANALMETR:40; :: thesis: verum

end;

( a9,b9 // a19,b19 & a9,c9 // a19,c19 ) by A40, ANALMETR:36;
then b9,c9 // b19,c19 by A31, A32, A33, A34, A41, A42, A43, A44, A49, A50, A51, A45, A46, A47, A52, A48, AFF_2:def 4;
hence b,c // b1,c1 by ANALMETR:36; :: thesis: verum

end;

hence MS is satisfying_DES by CONAFFM:def 1; :: thesis: verum

end;

hence ( MS is satisfying_DES iff AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian ) by A1; :: thesis: verum