let MS be OrtAfPl; :: thesis: ( MS is satisfying_des iff Af MS is translational )
set AS = Af MS;

A1: now

assume A2: MS is satisfying_des ; :: thesis: Af MS is translational

now

let A, P, C be Subset of (Af MS); :: thesis: for a, b, c, a', b', c' being Element of (Af MS) st A // P & A // 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 a, b, c, a', b', c' be Element of (Af MS); :: thesis: ( A // P & A // 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: ( A // P & A // C ) and
A4: ( a in A & a' in A & b in P & b' in P & c in C & c' in C ) and
A5: ( A is being_line & P is being_line & C is being_line ) and
A6: ( A <> P & A <> C ) and
A7: ( a,b // a',b' & a,c // a',c' ) ; :: thesis: b,c // b',c'
A8: ( not a in P & not a in C ) by A3, A4, A6, AFF_1:59;

A9: now

assume a = a' ; :: thesis: b,c // b',c'
then ( LIN a,b,b' & LIN a,c,c' ) by A7, AFF_1:def 1;
then ( LIN b,b',a & LIN c,c',a ) by AFF_1:15;
then ( b = b' & c = c' ) by A4, A5, A8, AFF_1:39;
hence b,c // b',c' by AFF_1:11; :: thesis: verum

end;

now

assume A10: a <> a' ; :: thesis: b,c // b',c'
reconsider aa = a, a1 = a', bb = b, b1 = b', cc = c, c1 = c' as Element of MS by ANALMETR:47;
A11: not LIN aa,a1,bb

proof

assume LIN aa,a1,bb ; :: thesis: contradiction
then LIN a,a',b by ANALMETR:55;
then b in A by A4, A5, A10, AFF_1:39;
hence contradiction by A3, A4, A6, AFF_1:59; :: thesis: verum

end;

A12: not LIN aa,a1,cc

proof

assume LIN aa,a1,cc ; :: thesis: contradiction
then LIN a,a',c by ANALMETR:55;
then c in A by A4, A5, A10, AFF_1:39;
hence contradiction by A3, A4, A6, AFF_1:59; :: thesis: verum

end;

A13: ( aa,a1 // bb,b1 & aa,a1 // cc,c1 )

proof

( a,a' // b,b' & a,a' // c,c' ) by A3, A4, AFF_1:53;
hence ( aa,a1 // bb,b1 & aa,a1 // cc,c1 ) by ANALMETR:48; :: thesis: verum

end;

( aa,bb // a1,b1 & aa,cc // a1,c1 ) by A7, ANALMETR:48;
then bb,cc // b1,c1 by A2, A11, A12, A13, CONMETR:def 8;
hence b,c // b',c' by ANALMETR:48; :: thesis: verum

end;

hence b,c // b',c' by A9; :: thesis: verum

end;

hence Af MS is translational by AFF_2:def 11; :: thesis: verum

end;

now

assume A14: Af MS is translational ; :: thesis: MS is satisfying_des

now

let a, a1, b, b1, c, c1 be Element of the carrier of MS; :: thesis: ( not LIN a,a1,b & not LIN a,a1,c & a,a1 // b,b1 & a,a1 // c,c1 & a,b // a1,b1 & a,c // a1,c1 implies b,c // b1,c1 )
assume that
A15: ( not LIN a,a1,b & not LIN a,a1,c ) and
A16: ( a,a1 // b,b1 & a,a1 // c,c1 ) and
A17: ( a,b // a1,b1 & a,c // a1,c1 ) ; :: thesis: b,c // b1,c1
reconsider a' = a, a1' = a1, b' = b, b1' = b1, c' = c, c1' = c1 as Element of (Af MS) by ANALMETR:47;
A18: ( not a',a1' // a',b' & not a',a1' // a',c' )

proof

assume ( a',a1' // a',b' or a',a1' // a',c' ) ; :: thesis: contradiction
then ( a,a1 // a,b or a,a1 // a,c ) by ANALMETR:48;
hence contradiction by A15, ANALMETR:def 11; :: thesis: verum

end;

A19: ( a',a1' // b',b1' & a',a1' // c',c1' ) by A16, ANALMETR:48;
A20: ( a',b' // a1',b1' & a',c' // a1',c1' ) by A17, ANALMETR:48;
A21: a' <> a1' by A18, AFF_1:12;
set A = Line a',a1';
A22: ( Line a',a1' is being_line & a' in Line a',a1' & a1' in Line a',a1' ) by A21, AFF_1:26, AFF_1:def 3;
then A23: a',a1' // Line a',a1' by AFF_1:37;
consider P being Subset of (Af MS) such that
A24: b' in P and
A25: Line a',a1' // P by A22, AFF_1:63;
consider C being Subset of (Af MS) such that
A26: c' in C and
A27: Line a',a1' // C by A22, AFF_1:63;
A28: ( P is being_line & C is being_line ) by A25, A27, AFF_1:50;
( a',a1' // P & a',a1' // C ) by A23, A25, A27, AFF_1:57;
then ( b',b1' // P & c',c1' // C ) by A19, A21, AFF_1:46;
then A29: ( b1' in P & c1' in C ) by A24, A26, A28, AFF_1:37;
A30: Line a',a1' <> P by A18, A22, A24, AFF_1:65;
Line a',a1' <> C by A18, A22, A26, AFF_1:65;
then b',c' // b1',c1' by A14, A20, A22, A24, A25, A26, A27, A28, A29, A30, AFF_2:def 11;
hence b,c // b1,c1 by ANALMETR:48; :: thesis: verum

end;

hence MS is satisfying_des by CONMETR:def 8; :: thesis: verum

end;

hence ( MS is satisfying_des iff Af MS is translational ) by A1; :: thesis: verum