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 :: 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 )
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;
now :: thesis: ( ( for x being Element of OAS holds p,x // p,f . x ) implies f is positive_dilatation )
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, Th64;
hence f is positive_dilatation by Th27; :: thesis: verum
end;
hence ( f is positive_dilatation or f is negative_dilatation ) by A4; :: thesis: verum
end;
now :: thesis: ( ( for x being Element of OAS holds f . x <> x ) implies f is positive_dilatation )
assume 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;
hence ( f is positive_dilatation or f is negative_dilatation ) by A2; :: thesis: verum