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 ; :: thesis: for a, b, c, a', b', c' being Element of 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 ; :: 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 and
A4: A // C and
A5: a in A and
A6: a' in A and
A7: b in P and
A8: b' in P and
A9: c in C and
A10: c' 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 // a',b' and
A17: a,c // a',c' ; :: thesis: b,c // b',c'
A18: not a in C by A4, A5, A15, AFF_1:59;

A19: now

reconsider aa = a, a1 = a', bb = b, b1 = b', cc = c, c1 = c' as Element of by ANALMETR:47;
a,a' // b,b' by A3, A5, A6, A7, A8, AFF_1:53;
then A20: aa,a1 // bb,b1 by ANALMETR:48;
a,a' // c,c' by A4, A5, A6, A9, A10, AFF_1:53;
then A21: aa,a1 // cc,c1 by ANALMETR:48;
assume A22: a <> a' ; :: thesis: b,c // b',c'
A23: 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 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,a',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 // b',c' by ANALMETR:48; :: thesis: verum

end;

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

now

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

end;

hence b,c // b',c' 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 ; :: 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 a' = a, a1' = a1, b' = b, b1' = b1, c' = c, c1' = c1 as Element of by ANALMETR:47;
A33: a',a1' // b',b1' by A30, ANALMETR:48;
A34: ( a',b' // a1',b1' & a',c' // a1',c1' ) by A32, ANALMETR:48;
A35: a',a1' // c',c1' by A31, ANALMETR:48;
set A = Line a',a1';
A36: ( 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 A29, ANALMETR:def 11; :: thesis: verum

end;

then A37: a' <> a1' by AFF_1:12;
then A38: Line a',a1' is being_line by AFF_1:def 3;
then consider C being Subset of such that
A39: c' in C and
A40: Line a',a1' // C by AFF_1:63;
A41: C is being_line by A40, AFF_1:50;
A42: ( a' in Line a',a1' & a1' in Line a',a1' ) by AFF_1:26;
then A43: Line a',a1' <> C by A36, A38, A39, AFF_1:65;
A44: a',a1' // Line a',a1' by A38, A42, AFF_1:37;
then a',a1' // C by A40, AFF_1:57;
then c',c1' // C by A35, A37, AFF_1:46;
then A45: c1' in C by A39, A41, AFF_1:37;
consider P being Subset of such that
A46: b' in P and
A47: Line a',a1' // P by A38, AFF_1:63;
A48: P is being_line by A47, AFF_1:50;
a',a1' // P by A44, A47, AFF_1:57;
then b',b1' // P by A33, A37, AFF_1:46;
then A49: b1' in P by A46, A48, AFF_1:37;
Line a',a1' <> P by A36, A38, A42, A46, AFF_1:65;
then b',c' // b1',c1' 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