ex Z being Subset of (LinearTopSpaceNorm X) st
( Z = Y & Cl Y = Cl Z ) by defcl;
hence Cl Y is closed by NORMSP_2:32; :: thesis: verum