for X being RealBanachSpace
for Y being RealNormSpace
for T being Lipschitzian LinearOperator of X,Y
for r being Real
for BX1 being Subset of (LinearTopSpaceNorm X)
for TBX1, BYr being Subset of (LinearTopSpaceNorm Y) st r > 0 & BYr = Ball ((0. Y),r) & TBX1 = T .: (Ball ((0. X),1)) & BYr c= Cl TBX1 holds
BYr c= TBX1