let X be OrtAfPl; :: thesis: ( X is satisfying_DES iff Af X is Desarguesian )
A1: ( X is satisfying_DES implies Af X is Desarguesian )

proof

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

now

let A, M, N be Subset of (Af X); :: thesis: for o, a, b, c, a1, b1, c1 being Element of (Af X) st o in A & o in M & o in N & o <> a & o <> b & o <> c & a in A & a1 in A & b in M & b1 in M & c in N & c1 in N & A is being_line & M is being_line & N is being_line & A <> M & A <> N & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1
let o, a, b, c, a1, b1, c1 be Element of (Af X); :: thesis: ( o in A & o in M & o in N & o <> a & o <> b & o <> c & a in A & a1 in A & b in M & b1 in M & c in N & c1 in N & A is being_line & M is being_line & N is being_line & A <> M & A <> N & a,b // a1,b1 & a,c // a1,c1 implies b,c // b1,c1 )
assume A3: ( o in A & o in M & o in N & o <> a & o <> b & o <> c & a in A & a1 in A & b in M & b1 in M & c in N & c1 in N & A is being_line & M is being_line & N is being_line & A <> M & A <> N & a,b // a1,b1 & a,c // a1,c1 ) ; :: thesis: b,c // b1,c1
assume A4: not b,c // b1,c1 ; :: thesis: contradiction
reconsider o' = o, a' = a, a1' = a1, b' = b, b1' = b1, c' = c, c1' = c1 as Element of X by ANALMETR:47;
A5: ( A // A & M // M & N // N ) by A3, AFF_1:55;
A6: ( LIN o',a',a1' & LIN o',b',b1' & LIN o',c',c1' )

proof

( o,a // o,a1 & o,b // o,b1 & o,c // o,c1 ) by A3, A5, AFF_1:53;
then ( LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 ) by AFF_1:def 1;
hence ( LIN o',a',a1' & LIN o',b',b1' & LIN o',c',c1' ) by ANALMETR:55; :: thesis: verum

end;

A7: ( o' <> a1' & o' <> b1' & o' <> c1' )

proof

assume A8: ( not o' <> a1' or not o' <> b1' or not o' <> c1' ) ; :: thesis: contradiction

A9: now

assume A10: o' = a1' ; :: thesis: contradiction
A11: o = b1

proof

assume A12: o <> b1 ; :: thesis: contradiction
A13: not LIN b,a,o

proof

assume LIN b,a,o ; :: thesis: contradiction
then LIN o,a,b by AFF_1:15;
then b in A by A3, AFF_1:39;
then ( o,b // A & o,b // M ) by A3, AFF_1:66;
then A // M by A3, AFF_1:67;
hence contradiction by A3, AFF_1:59; :: thesis: verum

end;

LIN o,b,b1 by A6, ANALMETR:55;
then A14: LIN b,o,b1 by AFF_1:15;
a,o // a,b1

proof

A15: o,b1 // o,b by A3, A5, AFF_1:53;
then a,b // o,b by A3, A10, A12, AFF_1:14;
then b,a // b,o by AFF_1:13;
then LIN b,a,o by AFF_1:def 1;
then LIN o,a,b by AFF_1:15;
then o,a // o,b by AFF_1:def 1;
then o,a // o,b1 by A3, A15, AFF_1:14;
then LIN o,a,b1 by AFF_1:def 1;
then LIN a,o,b1 by AFF_1:15;
hence a,o // a,b1 by AFF_1:def 1; :: thesis: verum

end;

hence contradiction by A12, A13, A14, AFF_1:23; :: thesis: verum

end;

o = c1

proof

assume A16: o <> c1 ; :: thesis: contradiction
A17: not LIN c,a,o

proof

assume LIN c,a,o ; :: thesis: contradiction
then LIN o,a,c by AFF_1:15;
then c in A by A3, AFF_1:39;
then ( o,c // A & o,c // N ) by A3, AFF_1:66;
then A // N by A3, AFF_1:67;
hence contradiction by A3, AFF_1:59; :: thesis: verum

end;

LIN o,c,c1 by A6, ANALMETR:55;
then A18: LIN c,o,c1 by AFF_1:15;
a,o // a,c1

proof

A19: o,c // o,c1 by A3, A5, AFF_1:53;
then a,c // o,c by A3, A10, A16, AFF_1:14;
then c,a // c,o by AFF_1:13;
then LIN c,a,o by AFF_1:def 1;
then LIN o,a,c by AFF_1:15;
then o,a // o,c by AFF_1:def 1;
then o,a // o,c1 by A3, A19, AFF_1:14;
then LIN o,a,c1 by AFF_1:def 1;
then LIN a,o,c1 by AFF_1:15;
hence a,o // a,c1 by AFF_1:def 1; :: thesis: verum

end;

hence contradiction by A16, A17, A18, AFF_1:23; :: thesis: verum

end;

hence contradiction by A4, A11, AFF_1:12; :: thesis: verum

end;

A20: now

assume A21: o' = b1' ; :: thesis: contradiction
A22: not LIN a,b,o

proof

assume LIN a,b,o ; :: thesis: contradiction
then LIN o,a,b by AFF_1:15;
then b in A by A3, AFF_1:39;
then ( o,b // A & o,b // M ) by A3, AFF_1:66;
then A // M by A3, AFF_1:67;
hence contradiction by A3, AFF_1:59; :: thesis: verum

end;

LIN o,a,a1 by A6, ANALMETR:55;
then A23: LIN a,o,a1 by AFF_1:15;
b,o // b,a1

proof

A24: a1,o // a,o by A3, A5, AFF_1:53;
then a,b // a,o by A3, A9, A21, AFF_1:14;
then LIN a,b,o by AFF_1:def 1;
then LIN o,b,a by AFF_1:15;
then o,b // o,a by AFF_1:def 1;
then o,b // a,o by AFF_1:13;
then o,b // a1,o by A3, A24, AFF_1:14;
then o,b // o,a1 by AFF_1:13;
then LIN o,b,a1 by AFF_1:def 1;
then LIN b,o,a1 by AFF_1:15;
hence b,o // b,a1 by AFF_1:def 1; :: thesis: verum

end;

hence contradiction by A9, A22, A23, AFF_1:23; :: thesis: verum

end;

now

assume A25: o' = c1' ; :: thesis: contradiction
A26: not LIN a,c,o

proof

assume LIN a,c,o ; :: thesis: contradiction
then LIN o,a,c by AFF_1:15;
then c in A by A3, AFF_1:39;
then ( o,c // A & o,c // N ) by A3, AFF_1:66;
then A // N by A3, AFF_1:67;
hence contradiction by A3, AFF_1:59; :: thesis: verum

end;

LIN o,a,a1 by A6, ANALMETR:55;
then A27: LIN a,o,a1 by AFF_1:15;
c,o // c,a1

proof

A28: a1,o // a,o by A3, A5, AFF_1:53;
then a,c // a,o by A3, A9, A25, AFF_1:14;
then LIN a,c,o by AFF_1:def 1;
then LIN o,c,a by AFF_1:15;
then o,c // o,a by AFF_1:def 1;
then o,c // a,o by AFF_1:13;
then o,c // a1,o by A3, A28, AFF_1:14;
then o,c // o,a1 by AFF_1:13;
then LIN o,c,a1 by AFF_1:def 1;
then LIN c,o,a1 by AFF_1:15;
hence c,o // c,a1 by AFF_1:def 1; :: thesis: verum

end;

hence contradiction by A9, A26, A27, AFF_1:23; :: thesis: verum

end;

hence contradiction by A8, A9, A20; :: thesis: verum

end;

A29: ( not LIN b',b1',a' & not LIN a',a1',c' )

proof

assume ( LIN b',b1',a' or LIN a',a1',c' ) ; :: thesis: contradiction
then A30: ( LIN b,b1,a or LIN a,a1,c ) by ANALMETR:55;
A31: a <> a1

proof

assume A32: a = a1 ; :: thesis: contradiction
A33: b = b1

proof

assume A34: b <> b1 ; :: thesis: contradiction
A35: not LIN o,a,b

proof

assume LIN o,a,b ; :: thesis: contradiction
then b in A by A3, AFF_1:39;
then A36: o,b // A by A3, AFF_1:66;
o,b // M by A3, AFF_1:66;
then A // M by A3, A36, AFF_1:67;
hence contradiction by A3, AFF_1:59; :: thesis: verum

end;

LIN o,b,b1 by A6, ANALMETR:55;
hence contradiction by A3, A32, A34, A35, AFF_1:23; :: thesis: verum

end;

c = c1

proof

assume A37: c <> c1 ; :: thesis: contradiction
A38: not LIN o,a,c

proof

assume LIN o,a,c ; :: thesis: contradiction
then c in A by A3, AFF_1:39;
then A39: o,c // A by A3, AFF_1:66;
o,c // N by A3, AFF_1:66;
then A // N by A3, A39, AFF_1:67;
hence contradiction by A3, AFF_1:59; :: thesis: verum

end;

LIN o,c,c1 by A6, ANALMETR:55;
hence contradiction by A3, A32, A37, A38, AFF_1:23; :: thesis: verum

end;

hence contradiction by A4, A33, AFF_1:11; :: thesis: verum

end;

b <> b1

proof

assume A40: b = b1 ; :: thesis: contradiction
A41: not LIN o,b,a

proof

assume LIN o,b,a ; :: thesis: contradiction
then a in M by A3, AFF_1:39;
then A42: o,a // M by A3, AFF_1:66;
o,a // A by A3, AFF_1:66;
then A // M by A3, A42, AFF_1:67;
hence contradiction by A3, AFF_1:59; :: thesis: verum

end;

A43: LIN o,a,a1 by A6, ANALMETR:55;
b,a // b,a1 by A3, A40, AFF_1:13;
hence contradiction by A31, A41, A43, AFF_1:23; :: thesis: verum

end;

then ( a in M or c in A ) by A3, A30, A31, AFF_1:39;
then A44: ( o,a // M or o,c // A ) by A3, AFF_1:66;
( o,a // A & o,c // N ) by A3, AFF_1:66;
then ( A // M or A // N ) by A3, A44, AFF_1:67;
hence contradiction by A3, AFF_1:59; :: thesis: verum

end;

( a',b' // a1',b1' & a',c' // a1',c1' ) by A3, ANALMETR:48;
then b',c' // b1',c1' by A2, A3, A6, A7, A29, CONAFFM:def 1;
hence contradiction by A4, ANALMETR:48; :: thesis: verum

end;

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

end;

( Af X is Desarguesian implies X is satisfying_DES )

proof

assume A45: Af X is Desarguesian ; :: thesis: X is satisfying_DES

now

let o', a', a1', b', b1', c', c1' be Element of X; :: 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 A46: ( 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' ) ; :: thesis: b',c' // b1',c1'
reconsider o = o', a = a', a1 = a1', b = b', b1 = b1', c = c', c1 = c1' as Element of (Af X) by ANALMETR:47;
A47: ( not LIN b,b1,a & not LIN a,a1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 ) by A46, ANALMETR:55;
then consider A being Subset of (Af X) such that
A48: ( A is being_line & o in A & a in A & a1 in A ) by AFF_1:33;
consider M being Subset of (Af X) such that
A49: ( M is being_line & o in M & b in M & b1 in M ) by A47, AFF_1:33;
consider N being Subset of (Af X) such that
A50: ( N is being_line & o in N & c in N & c1 in N ) by A47, AFF_1:33;
A51: ( A // A & M // M & N // N ) by A48, A49, A50, AFF_1:55;
A52: ( A <> M & A <> N )

proof

assume ( not A <> M or not A <> N ) ; :: thesis: contradiction
then ( b,b1 // b,a or a,a1 // a,c ) by A48, A49, A50, A51, AFF_1:53;
hence contradiction by A47, AFF_1:def 1; :: thesis: verum

end;

( a,b // a1,b1 & a,c // a1,c1 ) by A46, ANALMETR:48;
then b,c // b1,c1 by A45, A46, A48, A49, A50, A52, AFF_2:def 4;
hence b',c' // b1',c1' by ANALMETR:48; :: thesis: verum

end;

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

end;

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