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 )

A2: now

assume for x being Element of OAS holds f . x <> x ; :: thesis: f is positive_dilatation
then f is translation by A1, Def9;
hence f is positive_dilatation by Th73; :: thesis: verum

end;

now

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

A4: now

assume 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, Th79;
hence f is positive_dilatation by Th42; :: thesis: verum

end;

now

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, Th51;
then p,q // f . q,p by A5, DIRAF:def 4;
then q,p // p,f . q by DIRAF:5;
then ( Mid q,p,f . q & p <> q ) by A5, DIRAF:def 3;
hence f is negative_dilatation by A1, A3, Th78; :: thesis: verum

end;

hence ( f is positive_dilatation or f is negative_dilatation ) by A4; :: thesis: verum

end;

hence ( f is positive_dilatation or f is negative_dilatation ) by A2; :: thesis: verum