let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: z in r * (Cl A) ; :: thesis:
then reconsider z = z as Point of X ;

let G be Subset of X; :: thesis:
assume ( G is open & z in G ) ; :: thesis:
then A2: ( (r ") * z in (r ") * G & (r ") * G is open ) by Th49;
consider v being Point of X such that
A3: z = r * v and
A4: v in Cl A by A1;
(r ") * z = ((r ") * r) * v by A3, RLVECT_1:def 7
.= 1 * v by XCMPLX_0:def 7
.= v by RLVECT_1:def 8 ;
then A meets (r ") * G by A4, A2, PRE_TOPC:24;
then consider x being object such that
A5: x in A and
A6: x in (r ") * G by XBOOLE_0:3;
reconsider x = x as Point of X by A5;
consider u being Point of X such that
A7: x = (r ") * u and
A8: u in G by A6;
A9: r * x in r * A by A5;
r * x = (r * (r ")) * u by A7, RLVECT_1:def 7
.= 1 * u by XCMPLX_0:def 7
.= u by RLVECT_1:def 8 ;
hence r * A meets G by A8, A9, XBOOLE_0:3; :: thesis:

end;

end;