let OAS be OAffinSpace; :: thesis: for f being Permutation of the carrier of OAS holds
( not f is negative_dilatation or not f is positive_dilatation )
given f being Permutation of the carrier of OAS such that A1: ( f is negative_dilatation & f is positive_dilatation ) ; :: thesis: contradiction
consider a, b being Element of OAS such that
A2: a <> b by STRUCT_0:def 10;
( a,b // f . a,f . b & a,b // f . b,f . a ) by A1, Th27;
then f . a,f . b // f . b,f . a by A2, ANALOAF:def 5;
then f . a = f . b by ANALOAF:def 5;
hence contradiction by A2, FUNCT_2:58; :: thesis: verum