let OAS be OAffinSpace; :: thesis: for x, y being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation & LIN x,f . x,y holds
LIN x,f . x,f . y
let x, y be Element of OAS; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation & LIN x,f . x,y holds
LIN x,f . x,f . y
let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation & LIN x,f . x,y implies LIN x,f . x,f . y )
assume A1: f is dilatation ; :: thesis: ( not LIN x,f . x,y or LIN x,f . x,f . y )
assume A2: LIN x,f . x,y ; :: thesis: LIN x,f . x,f . y

now

assume A3: x <> y ; :: thesis: LIN x,f . x,f . y
( x,f . x '||' x,y & x,y '||' f . x,f . y ) by A1, A2, Th51, DIRAF:def 5;
then x,f . x '||' f . x,f . y by A3, DIRAF:23;
then f . x,x '||' f . x,f . y by DIRAF:22;
then LIN f . x,x,f . y by DIRAF:def 5;
hence LIN x,f . x,f . y by DIRAF:30; :: thesis: verum

end;

hence LIN x,f . x,f . y by DIRAF:31; :: thesis: verum