let MS be OrtAfPl; :: thesis: ( MS is satisfying_DES iff Af MS is Desarguesian )
set AS = Af MS;

A1: now

assume A2: MS is satisfying_DES ; :: thesis: Af MS is Desarguesian

now

let A, P, C be Subset of (Af MS); :: thesis: for o, a, b, c, a', b', c' being Element of the carrier of (Af MS) 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 the carrier of (Af MS); :: 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'

now

assume A9: ( o <> a' & a <> a' ) ; :: thesis: b,c // b',c'
then A10: ( b <> b' & c <> c' ) by A3, A4, A5, A6, A7, A8, AFF_4:9;

A11: now

assume LIN b,b',a ; :: thesis: contradiction
then a in P by A5, A6, A10, AFF_1:39;
hence contradiction by A3, A4, A5, A6, A7, AFF_1:30; :: thesis: verum

end;

A12: now

assume LIN a,a',c ; :: thesis: contradiction
then c in A by A5, A6, A9, AFF_1:39;
hence contradiction by A3, A4, A5, A6, A7, AFF_1:30; :: thesis: verum

end;

reconsider o1 = o, a1 = a, b1 = b, c1 = c, a1' = a', b1' = b', c1' = c' as Element of MS by ANALMETR:47;
A13: ( o1 <> a1 & o1 <> b1 & o1 <> c1 & o1 <> a1' & o1 <> b1' & o1 <> c1' ) by A3, A4, A5, A6, A7, A8, A9, AFF_4:8;
( LIN o,a,a' & LIN o,b,b' & LIN o,c,c' ) by A3, A5, A6, AFF_1:33;
then A14: ( LIN o1,a1,a1' & LIN o1,b1,b1' & LIN o1,c1,c1' ) by ANALMETR:55;
A15: ( a1,b1 // a1',b1' & a1,c1 // a1',c1' ) by A8, ANALMETR:48;
A16: not LIN b1,b1',a1 by A11, ANALMETR:55;
not LIN a1,a1',c1 by A12, ANALMETR:55;
then b1,c1 // b1',c1' by A2, A13, A14, A15, A16, CONAFFM:def 1;
hence b,c // b',c' by ANALMETR:48; :: thesis: verum

end;

hence b,c // b',c' by A3, A4, A5, A6, A7, A8, AFPROJ:50; :: thesis: verum

end;

hence Af MS is Desarguesian by AFF_2:def 4; :: thesis: verum

end;

now

assume A17: Af MS is Desarguesian ; :: thesis: MS is satisfying_DES

now

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
A18: ( o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 ) and
A19: ( not LIN b,b1,a & not LIN a,a1,c ) and
A20: ( LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 ) and
A21: ( a,b // a1,b1 & a,c // a1,c1 ) ; :: thesis: b,c // b1,c1
reconsider o' = o, a' = a, b' = b, c' = c, a1' = a1, b1' = b1, c1' = c1 as Element of (Af MS) by ANALMETR:47;
A22: ( a',b' // a1',b1' & a',c' // a1',c1' ) by A21, ANALMETR:48;
A23: ( LIN o',a',a1' & LIN o',b',b1' & LIN o',c',c1' ) by A20, ANALMETR:55;
then consider A being Subset of (Af MS) such that
A24: A is being_line and
A25: ( o' in A & a' in A & a1' in A ) by AFF_1:33;
consider P being Subset of (Af MS) such that
A26: P is being_line and
A27: ( o' in P & b' in P & b1' in P ) by A23, AFF_1:33;
consider C being Subset of (Af MS) such that
A28: C is being_line and
A29: ( o' in C & c' in C & c1' in C ) by A23, AFF_1:33;
A30: A <> P

proof

assume A = P ; :: thesis: contradiction
then LIN b',b1',a' by A25, A26, A27, AFF_1:33;
hence contradiction by A19, ANALMETR:55; :: thesis: verum

end;

A <> C

proof

assume A = C ; :: thesis: contradiction
then LIN a',a1',c' by A24, A25, A29, AFF_1:33;
hence contradiction by A19, ANALMETR:55; :: thesis: verum

end;

then b',c' // b1',c1' by A17, A18, A22, A24, A25, A26, A27, A28, A29, A30, AFF_2:def 4;
hence b,c // b1,c1 by ANALMETR:48; :: thesis: verum

end;

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

end;

hence ( MS is satisfying_DES iff Af MS is Desarguesian ) by A1; :: thesis: verum