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 ; :: according to CONMETR:def 8 :: thesis: for a1, b, b1, c, c1 being Element of 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 ; :: 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
A2: not LIN a,a1,b and
A3: not LIN a,a1,c and
A4: a,a1 // b,b1 and
A5: a,a1 // c,c1 and
A6: a,b // a1,b1 and
A7: 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;
LIN a',a1',a1' by AFF_1:16;
then consider A' being Subset of such that
A8: A' is being_line and
A9: a' in A' and
A10: a1' in A' and
a1' in A' by AFF_1:33;
A11: a',b' // a1',b1' by A6, ANALMETR:48;
b,b1 // a,a1 by A4, ANALMETR:81;
then A12: b',b1' // a',a1' by ANALMETR:48;
A13: 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 holds
( x' in A' iff LIN a',a1',x' ) by A8, A9, A10, AFF_1:33, AFF_1:39;
then A' = Line a',a1' by AFF_1:def 2;
then A14: b',b1' // A' by A13, A12, AFF_1:def 4;
A15: a',c' // a1',c1' by A7, ANALMETR:48;
c,c1 // a,a1 by A5, ANALMETR:81;
then A16: c',c1' // a',a1' by ANALMETR:48;
A17: 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 holds
( x' in A' iff LIN a',a1',x' ) by A8, A9, A10, AFF_1:33, AFF_1:39;
then A' = Line a',a1' by AFF_1:def 2;
then A18: c',c1' // A' by A17, A16, AFF_1:def 4;
LIN c',c1',c1' by AFF_1:16;
then consider N' being Subset of such that
A19: N' is being_line and
A20: c' in N' and
A21: c1' in N' and
c1' in N' by AFF_1:33;
LIN b',b1',b1' by AFF_1:16;
then consider M' being Subset of such that
A22: M' is being_line and
A23: b' in M' and
A24: b1' in M' and
b1' in M' by AFF_1:33;
A25: ( A' <> M' & A' <> N' )

proof

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

end;

A26: c' <> c1'

proof

assume c' = c1' ; :: thesis: contradiction
then c,a // c,a1 by A7, 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 A3, ANALMETR:55; :: thesis: verum

end;

then for x' being Element of holds
( x' in N' iff LIN c',c1',x' ) by A19, A20, A21, AFF_1:33, AFF_1:39;
then N' = Line c',c1' by AFF_1:def 2;
then A27: A' // N' by A18, A26, AFF_1:def 5;
A28: b' <> b1'

proof

assume b' = b1' ; :: thesis: contradiction
then b,a // b,a1 by A6, 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 holds
( x' in M' iff LIN b',b1',x' ) by A22, A23, A24, AFF_1:33, AFF_1:39;
then M' = Line b',b1' by AFF_1:def 2;
then A' // M' by A14, A28, AFF_1:def 5;
then b',c' // b1',c1' by A1, A8, A9, A10, A22, A23, A24, A19, A20, A21, A27, A25, A11, A15, AFF_2:def 11;
hence b,c // b1,c1 by ANALMETR:48; :: thesis: verum