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 LIN p,y,z holds
y,z // f . y,f . z

proof

let y, z be Element of OAS; :: thesis: ( not LIN p,y,z implies y,z // f . y,f . z )
assume A5: not LIN p,y,z ; :: thesis: y,z // f . y,f . z
( p,y // p,f . y & p,z // p,f . z & y,z '||' f . y,f . z ) by A1, A3, Th51;
hence y,z // f . y,f . z by A5, PASCH:20; :: thesis: verum

end;

let y, z be Element of OAS; :: thesis: y,z // f . y,f . z
( LIN p,y,z implies y,z // f . y,f . z )

proof

assume A6: LIN p,y,z ; :: thesis: y,z // f . y,f . z

A7: now

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:5; :: thesis: verum

end;

now

assume A8: ( p <> y & y <> z & z <> p ) ; :: thesis: y,z // f . y,f . z
then consider q being Element of OAS such that
A9: not LIN p,y,q by DIRAF:43;
consider r being Element of OAS such that
A10: y,z '||' q,r and
A11: y,q '||' z,r by DIRAF:31;
A12: not LIN y,z,q

proof

assume LIN y,z,q ; :: thesis: contradiction
then ( LIN y,z,q & LIN y,z,p & LIN y,z,y ) by A6, DIRAF:36, DIRAF:37;
hence contradiction by A8, A9, DIRAF:38; :: thesis: verum

end;

then A13: y,z // q,r by A10, A11, PASCH:21;
A14: q <> r

proof

assume q = r ; :: thesis: contradiction
then q,y '||' q,z by A11, DIRAF:27;
then LIN q,y,z by DIRAF:def 5;
hence contradiction by A12, DIRAF:36; :: thesis: verum

end;

not LIN p,q,r

proof

assume LIN p,q,r ; :: thesis: contradiction
then A15: LIN q,r,p by DIRAF:36;
LIN y,p,z by A6, DIRAF:36;
then y,p '||' y,z by DIRAF:def 5;
then y,z '||' p,y by DIRAF:27;
then q,r '||' p,y by A8, A10, DIRAF:28;
then ( LIN q,r,y & LIN q,r,q ) by A14, A15, DIRAF:37, DIRAF:39;
hence contradiction by A9, A14, A15, DIRAF:38; :: thesis: verum

end;

then A16: q,r // f . q,f . r by A4;
A17: f . y,f . z '||' f . q,f . r by A1, A10, Th58;
A18: f . y,f . q '||' f . z,f . r by A1, A11, Th58;
not LIN f . y,f . z,f . q by A1, A12, Th59;
then f . y,f . z // f . q,f . r by A17, A18, PASCH:21;
then A19: f . q,f . r // f . y,f . z by DIRAF:5;
y,z // f . q,f . r by A13, A14, A16, DIRAF:6;
hence y,z // f . y,f . z by A14, A19, DIRAF:6, FUNCT_2:85; :: thesis: verum

end;

hence y,z // f . y,f . z by A2, A3, A7, DIRAF:7; :: thesis: verum

end;

hence y,z // f . y,f . z by A4; :: thesis: verum