let X be OrtAfPl; :: thesis: ( Af X is translational iff X is satisfying_des )
( X is satisfying_des implies Af X is translational )

proof

assume A1: X is satisfying_des ; :: thesis: Af X is translational

now

let A, M, N be Subset of (Af X); :: thesis: for a, b, c, a1, b1, c1 being Element of (Af X) st A // M & A // N & 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 a, b, c, a1, b1, c1 be Element of (Af X); :: thesis: ( A // M & A // N & 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 A2: ( A // M & A // N & 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
reconsider a' = a, a1' = a1, b' = b, b1' = b1, c' = c, c1' = c1 as Element of X by ANALMETR:47;
b,c // b1,c1

proof

assume A3: not b,c // b1,c1 ; :: thesis: contradiction
A4: a <> a1

proof

assume A5: a = a1 ; :: thesis: contradiction
A6: b = b1

proof

assume A7: b <> b1 ; :: thesis: contradiction
LIN a,b,b1 by A2, A5, AFF_1:def 1;
then LIN b,b1,a by AFF_1:15;
then a in M by A2, A7, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

c = c1

proof

assume A8: c <> c1 ; :: thesis: contradiction
LIN a,c,c1 by A2, A5, AFF_1:def 1;
then LIN c,c1,a by AFF_1:15;
then a in N by A2, A8, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

hence contradiction by A3, A6, AFF_1:11; :: thesis: verum

end;

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

proof

assume ( LIN a',a1',b' or LIN a',a1',c' ) ; :: thesis: contradiction
then ( LIN a,a1,b or LIN a,a1,c ) by ANALMETR:55;
then ( b in A or c in A ) by A2, A4, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum

end;

( a,a1 // b,b1 & a,a1 // c,c1 ) by A2, AFF_1:53;
then A10: ( a',a1' // b',b1' & a',a1' // c',c1' ) by ANALMETR:48;
( a',b' // a1',b1' & a',c' // a1',c1' ) by A2, ANALMETR:48;
then b',c' // b1',c1' by A1, A9, A10, CONMETR:def 8;
hence contradiction by A3, ANALMETR:48; :: thesis: verum

end;

hence b,c // b1,c1 ; :: thesis: verum

end;

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

end;

hence ( Af X is translational iff X is satisfying_des ) by CONMETR:8; :: thesis: verum