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
A6: ( p,y // p,f . y & p,z // p,f . z ) by A3;
y,z '||' f . y,f . z by A1, Th51;
hence y,z // f . y,f . z by A5, A6, 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 A7: LIN p,y,z ; :: thesis: y,z // f . y,f . z

A8: now

assume that
A9: p <> y and
A10: y <> z and
z <> p ; :: thesis: y,z // f . y,f . z
consider q being Element of OAS such that
A11: not LIN p,y,q by A9, DIRAF:43;
A12: not LIN y,z,q

proof

assume A13: LIN y,z,q ; :: thesis: contradiction
( LIN y,z,p & LIN y,z,y ) by A7, DIRAF:36, DIRAF:37;
hence contradiction by A10, A11, A13, DIRAF:38; :: thesis: verum

end;

then A14: not LIN f . y,f . z,f . q by A1, Th59;
consider r being Element of OAS such that
A15: y,z '||' q,r and
A16: y,q '||' z,r by DIRAF:31;
( f . y,f . z '||' f . q,f . r & f . y,f . q '||' f . z,f . r ) by A1, A15, A16, Th58;
then f . y,f . z // f . q,f . r by A14, PASCH:21;
then A17: f . q,f . r // f . y,f . z by DIRAF:5;
A18: q <> r

proof

assume q = r ; :: thesis: contradiction
then q,y '||' q,z by A16, 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

A19: LIN q,r,q by DIRAF:37;
assume LIN p,q,r ; :: thesis: contradiction
then A20: LIN q,r,p by DIRAF:36;
LIN y,p,z by A7, 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 A10, A15, DIRAF:28;
then LIN q,r,y by A18, A20, DIRAF:39;
hence contradiction by A11, A18, A20, A19, DIRAF:38; :: thesis: verum

end;

then A21: q,r // f . q,f . r by A4;
y,z // q,r by A15, A16, A12, PASCH:21;
then y,z // f . q,f . r by A18, A21, DIRAF:6;
hence y,z // f . y,f . z by A18, A17, DIRAF:6, FUNCT_2:85; :: thesis: verum

end;

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;

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

end;

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