let X be OrtAfPl; :: thesis: ( X is satisfying_TDES iff Af X is Moufangian )
( Af X is Moufangian implies X is satisfying_TDES )

proof

assume A1: Af X is Moufangian ; :: thesis: X is satisfying_TDES

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 b',b1',c' & LIN o',a',a1' & LIN o',b',b1' & LIN o',c',c1' & a',b' // a1',b1' & a',b' // o',c' & b',c' // b1',c1' implies a',c' // a1',c1' )
assume A2: ( o' <> a' & o' <> a1' & o' <> b' & o' <> b1' & o' <> c' & o' <> c1' & not LIN b',b1',a' & not LIN b',b1',c' & LIN o',a',a1' & LIN o',b',b1' & LIN o',c',c1' & a',b' // a1',b1' & a',b' // o',c' & b',c' // b1',c1' ) ; :: thesis: a',c' // a1',c1'
reconsider o = o', a = a', a1 = a1', b = b', b1 = b1', c = c', c1 = c1' as Element of the carrier of (Af X) by ANALMETR:47;
A3: ( not LIN b,b1,a & not LIN b,b1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 ) by A2, ANALMETR:55;
A4: ( a,b // a1,b1 & a,b // o,c & b,c // b1,c1 ) by A2, ANALMETR:48;
consider M being Subset of (Af X) such that
A5: ( M is being_line & o in M & c in M & c1 in M ) by A3, AFF_1:33;
A6: M // M by A5, AFF_1:55;
A7: not b in M

proof

assume b in M ; :: thesis: contradiction
then A8: o,b // b,c by A5, A6, AFF_1:53;
LIN b,b1,o by A3, AFF_1:15;
then b,b1 // b,o by AFF_1:def 1;
then b,b1 // o,b by AFF_1:13;
then b,b1 // b,c by A2, A8, AFF_1:14;
hence contradiction by A3, AFF_1:def 1; :: thesis: verum

end;

A9: ( o <> c & b <> a ) by A2, A3, AFF_1:16;
A10: ( b,a // b1,a1 & b,c // b1,c1 ) by A4, AFF_1:13;
b,a // o,c by A4, AFF_1:13;
then b,a // M by A2, A5, AFF_1:41;
then a,c // a1,c1 by A1, A3, A5, A7, A9, A10, AFF_2:def 7;
hence a',c' // a1',c1' by ANALMETR:48; :: thesis: verum

end;

hence X is satisfying_TDES by CONMETR:def 5; :: thesis: verum

end;

hence ( X is satisfying_TDES iff Af X is Moufangian ) by CONMETR:7; :: thesis: verum