let OAS be OAffinSpace; :: thesis: for p being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & ( for x being Element of OAS holds p,x // p,f . x ) holds
for y, z being Element of OAS holds y,z // f . y,f . z

let p be Element of OAS; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & ( for x being Element of OAS holds p,x // p,f . x ) holds
for y, z being Element of OAS holds y,z // f . y,f . z

let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation & f . p = p & ( for x being Element of OAS holds p,x // p,f . x ) implies for y, z being Element of OAS holds y,z // f . y,f . z )
assume that
A1: f is dilatation and
A2: f . p = p and
A3: for x being Element of OAS holds p,x // p,f . x ; :: thesis: for y, z being Element of OAS holds y,z // f . y,f . z
A4: for y, z being Element of OAS st not p,y,z are_collinear holds
y,z // f . y,f . z
proof
let y, z be Element of OAS; :: thesis: ( not p,y,z are_collinear implies y,z // f . y,f . z )
assume A5: not p,y,z are_collinear ; :: thesis: y,z // f . y,f . z
A6: ( p,y // p,f . y & p,z // p,f . z ) by A3;
y,z '||' f . y,f . z by ;
hence y,z // f . y,f . z by ; :: thesis: verum
end;
let y, z be Element of OAS; :: thesis: y,z // f . y,f . z
( p,y,z are_collinear implies y,z // f . y,f . z )
proof
assume A7: p,y,z are_collinear ; :: thesis: y,z // f . y,f . z
A8: now :: thesis: ( p <> y & y <> z & z <> p implies y,z // f . y,f . z )end;
now :: thesis: ( p = z implies y,z // f . y,f . z )
assume p = z ; :: thesis: y,z // f . y,f . z
then z,y // f . z,f . y by A2, A3;
hence y,z // f . y,f . z by DIRAF:2; :: thesis: verum
end;
hence y,z // f . y,f . z by ; :: thesis: verum
end;
hence y,z // f . y,f . z by A4; :: thesis: verum