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, a9, b9, c9 being Element of (Af MS) st A // P & A // 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, b, c, a9, b9, c9 be Element of (Af MS); :: thesis: ( A // P & A // 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: A // P and
A4: A // C and
A5: a in A and
A6: a9 in A and
A7: b in P and
A8: b9 in P and
A9: c in C and
A10: c9 in C and
A11: A is being_line and
A12: P is being_line and
A13: C is being_line and
A14: A <> P and
A15: A <> C and
A16: a,b // a9,b9 and
A17: a,c // a9,c9 ; :: thesis: b,c // b9,c9
A18: not a in C by A4, A5, A15, AFF_1:59;

A19: now

reconsider aa = a, a1 = a9, bb = b, b1 = b9, cc = c, c1 = c9 as Element of MS by ANALMETR:47;
a,a9 // b,b9 by A3, A5, A6, A7, A8, AFF_1:53;
then A20: aa,a1 // bb,b1 by ANALMETR:48;
a,a9 // c,c9 by A4, A5, A6, A9, A10, AFF_1:53;
then A21: aa,a1 // cc,c1 by ANALMETR:48;
assume A22: a <> a9 ; :: thesis: b,c // b9,c9
A23: not LIN aa,a1,bb

proof

assume LIN aa,a1,bb ; :: thesis: contradiction
then LIN a,a9,b by ANALMETR:55;
then b in A by A5, A6, A11, A22, AFF_1:39;
hence contradiction by A3, A7, A14, AFF_1:59; :: thesis: verum

end;

A24: not LIN aa,a1,cc

proof

assume LIN aa,a1,cc ; :: thesis: contradiction
then LIN a,a9,c by ANALMETR:55;
then c in A by A5, A6, A11, A22, AFF_1:39;
hence contradiction by A4, A9, A15, AFF_1:59; :: thesis: verum

end;

( aa,bb // a1,b1 & aa,cc // a1,c1 ) by A16, A17, ANALMETR:48;
then bb,cc // b1,c1 by A2, A23, A24, A20, A21, CONMETR:def 8;
hence b,c // b9,c9 by ANALMETR:48; :: thesis: verum

end;

A25: not a in P by A3, A5, A14, AFF_1:59;

now

assume A26: a = a9 ; :: thesis: b,c // b9,c9
then LIN a,c,c9 by A17, AFF_1:def 1;
then LIN c,c9,a by AFF_1:15;
then A27: c = c9 by A9, A10, A13, A18, AFF_1:39;
LIN a,b,b9 by A16, A26, AFF_1:def 1;
then LIN b,b9,a by AFF_1:15;
then b = b9 by A7, A8, A12, A25, AFF_1:39;
hence b,c // b9,c9 by A27, AFF_1:11; :: thesis: verum

end;

hence b,c // b9,c9 by A19; :: thesis: verum

end;

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

end;

now

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

now

let a, a1, b, b1, c, c1 be Element 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
A29: ( not LIN a,a1,b & not LIN a,a1,c ) and
A30: a,a1 // b,b1 and
A31: a,a1 // c,c1 and
A32: ( a,b // a1,b1 & a,c // a1,c1 ) ; :: thesis: b,c // b1,c1
reconsider a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1 as Element of (Af MS) by ANALMETR:47;
A33: a9,a19 // b9,b19 by A30, ANALMETR:48;
A34: ( a9,b9 // a19,b19 & a9,c9 // a19,c19 ) by A32, ANALMETR:48;
A35: a9,a19 // c9,c19 by A31, ANALMETR:48;
set A = Line a9,a19;
A36: ( not a9,a19 // a9,b9 & not a9,a19 // a9,c9 )

proof

assume ( a9,a19 // a9,b9 or a9,a19 // a9,c9 ) ; :: thesis: contradiction
then ( a,a1 // a,b or a,a1 // a,c ) by ANALMETR:48;
hence contradiction by A29, ANALMETR:def 11; :: thesis: verum

end;

then A37: a9 <> a19 by AFF_1:12;
then A38: Line a9,a19 is being_line by AFF_1:def 3;
then consider C being Subset of (Af MS) such that
A39: c9 in C and
A40: Line a9,a19 // C by AFF_1:63;
A41: C is being_line by A40, AFF_1:50;
A42: ( a9 in Line a9,a19 & a19 in Line a9,a19 ) by AFF_1:26;
then A43: Line a9,a19 <> C by A36, A38, A39, AFF_1:65;
A44: a9,a19 // Line a9,a19 by A38, A42, AFF_1:37;
then a9,a19 // C by A40, AFF_1:57;
then c9,c19 // C by A35, A37, AFF_1:46;
then A45: c19 in C by A39, A41, AFF_1:37;
consider P being Subset of (Af MS) such that
A46: b9 in P and
A47: Line a9,a19 // P by A38, AFF_1:63;
A48: P is being_line by A47, AFF_1:50;
a9,a19 // P by A44, A47, AFF_1:57;
then b9,b19 // P by A33, A37, AFF_1:46;
then A49: b19 in P by A46, A48, AFF_1:37;
Line a9,a19 <> P by A36, A38, A42, A46, AFF_1:65;
then b9,c9 // b19,c19 by A28, A34, A38, A42, A46, A47, A39, A40, A48, A41, A49, A45, A43, 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