let X be OrtAfPl; :: thesis: ( Af X is translational implies X is satisfying_des )
assume A1: Af X is translational ; :: thesis: X is satisfying_des
let a be Element of X; :: according to CONMETR:def 8 :: thesis: for a1, b, b1, c, c1 being Element of X st 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 holds
b,c // b1,c1
let a1, b, b1, c, c1 be Element of X; :: 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 A2: ( 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 ) ; :: thesis: b,c // b1,c1
reconsider a' = a, a1' = a1, b' = b, b1' = b1, c' = c, c1' = c1 as Element of (Af X) by ANALMETR:47;
LIN a',a1',a1' by AFF_1:16;
then consider A' being Subset of (Af X) such that
A3: ( A' is being_line & a' in A' & a1' in A' & a1' in A' ) by AFF_1:33;
LIN b',b1',b1' by AFF_1:16;
then consider M' being Subset of (Af X) such that
A4: ( M' is being_line & b' in M' & b1' in M' & b1' in M' ) by AFF_1:33;
LIN c',c1',c1' by AFF_1:16;
then consider N' being Subset of (Af X) such that
A5: ( N' is being_line & c' in N' & c1' in N' & c1' in N' ) by AFF_1:33;
A6: A' // M'

proof

A7: a' <> a1'

proof

assume a' = a1' ; :: thesis: contradiction
then LIN a',a1',b' by AFF_1:16;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

then for x' being Element of (Af X) holds
( x' in A' iff LIN a',a1',x' ) by A3, AFF_1:33, AFF_1:39;
then A8: A' = Line a',a1' by AFF_1:def 2;
b,b1 // a,a1 by A2, ANALMETR:81;
then b',b1' // a',a1' by ANALMETR:48;
then A9: b',b1' // A' by A7, A8, AFF_1:def 4;
A10: b' <> b1'

proof

assume b' = b1' ; :: thesis: contradiction
then b,a // b,a1 by A2, ANALMETR:81;
then LIN b,a,a1 by ANALMETR:def 11;
then LIN b',a',a1' by ANALMETR:55;
then LIN a',a1',b' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

then for x' being Element of (Af X) holds
( x' in M' iff LIN b',b1',x' ) by A4, AFF_1:33, AFF_1:39;
then M' = Line b',b1' by AFF_1:def 2;
hence A' // M' by A9, A10, AFF_1:def 5; :: thesis: verum

end;

A11: A' // N'

proof

A12: a' <> a1'

proof

assume a' = a1' ; :: thesis: contradiction
then LIN a',a1',b' by AFF_1:16;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

A13: A' = Line a',a1'

proof

for x' being Element of (Af X) holds
( x' in A' iff LIN a',a1',x' ) by A3, A12, AFF_1:33, AFF_1:39;
hence A' = Line a',a1' by AFF_1:def 2; :: thesis: verum

end;

c',c1' // a',a1'

proof

c,c1 // a,a1 by A2, ANALMETR:81;
hence c',c1' // a',a1' by ANALMETR:48; :: thesis: verum

end;

then A14: c',c1' // A' by A12, A13, AFF_1:def 4;
A15: c' <> c1'

proof

assume c' = c1' ; :: thesis: contradiction
then c,a // c,a1 by A2, ANALMETR:81;
then LIN c,a,a1 by ANALMETR:def 11;
then LIN c',a',a1' by ANALMETR:55;
then LIN a',a1',c' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

N' = Line c',c1'

proof

for x' being Element of (Af X) holds
( x' in N' iff LIN c',c1',x' ) by A5, A15, AFF_1:33, AFF_1:39;
hence N' = Line c',c1' by AFF_1:def 2; :: thesis: verum

end;

hence A' // N' by A14, A15, AFF_1:def 5; :: thesis: verum

end;

A16: ( A' <> M' & A' <> N' )

proof

assume ( A' = M' or A' = N' ) ; :: thesis: contradiction
then ( LIN a',a1',b' or LIN a',a1',c' ) by A3, A4, A5, AFF_1:33;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

A17: a',b' // a1',b1' by A2, ANALMETR:48;
a',c' // a1',c1' by A2, ANALMETR:48;
then b',c' // b1',c1' by A1, A3, A4, A5, A6, A11, A16, A17, AFF_2:def 11;
hence b,c // b1,c1 by ANALMETR:48; :: thesis: verum