let OAS be OAffinSpace; :: thesis: for f being Permutation of the carrier of OAS holds

( not f is dilatation or f is positive_dilatation or f is negative_dilatation )

let f be Permutation of the carrier of OAS; :: thesis: ( not f is dilatation or f is positive_dilatation or f is negative_dilatation )

assume A1: f is dilatation ; :: thesis: ( f is positive_dilatation or f is negative_dilatation )

( not f is dilatation or f is positive_dilatation or f is negative_dilatation )

let f be Permutation of the carrier of OAS; :: thesis: ( not f is dilatation or f is positive_dilatation or f is negative_dilatation )

assume A1: f is dilatation ; :: thesis: ( f is positive_dilatation or f is negative_dilatation )

A2: now :: thesis: ( for p being Element of OAS holds not f . p = p or f is positive_dilatation or f is negative_dilatation )

given p being Element of OAS such that A3:
f . p = p
; :: thesis: ( f is positive_dilatation or f is negative_dilatation )

end;A4: now :: thesis: ( not for q being Element of OAS holds p,q // p,f . q implies f is negative_dilatation )

given q being Element of OAS such that A5:
not p,q // p,f . q
; :: thesis: f is negative_dilatation

p,q '||' p,f . q by A1, A3, Th34;

then A6: p,q // f . q,p by A5, DIRAF:def 4;

then q,p // p,f . q by DIRAF:2;

then A7: Mid q,p,f . q by DIRAF:def 3;

p <> q by A5, A6, DIRAF:2;

hence f is negative_dilatation by A1, A3, A7, Th63; :: thesis: verum

end;p,q '||' p,f . q by A1, A3, Th34;

then A6: p,q // f . q,p by A5, DIRAF:def 4;

then q,p // p,f . q by DIRAF:2;

then A7: Mid q,p,f . q by DIRAF:def 3;

p <> q by A5, A6, DIRAF:2;

hence f is negative_dilatation by A1, A3, A7, Th63; :: thesis: verum

now :: thesis: ( ( for x being Element of OAS holds p,x // p,f . x ) implies f is positive_dilatation )

hence
( f is positive_dilatation or f is negative_dilatation )
by A4; :: thesis: verumassume
for x being Element of OAS holds p,x // p,f . x
; :: thesis: f is positive_dilatation

then for x, y being Element of OAS holds x,y // f . x,f . y by A1, A3, Th64;

hence f is positive_dilatation by Th27; :: thesis: verum

end;then for x, y being Element of OAS holds x,y // f . x,f . y by A1, A3, Th64;

hence f is positive_dilatation by Th27; :: thesis: verum

now :: thesis: ( ( for x being Element of OAS holds f . x <> x ) implies f is positive_dilatation )

hence
( f is positive_dilatation or f is negative_dilatation )
by A2; :: thesis: verumassume
for x being Element of OAS holds f . x <> x
; :: thesis: f is positive_dilatation

then f is translation by A1;

hence f is positive_dilatation by Th58; :: thesis: verum

end;then f is translation by A1;

hence f is positive_dilatation by Th58; :: thesis: verum