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

( 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