reconsider Z = Y as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
Cl Z is Subset of X by NORMSP_2:def 4;
hence ( ex b₁ being Subset of X ex Z being Subset of (LinearTopSpaceNorm X) st
( Z = Y & b₁ = Cl Z ) & ( for b₁, b₂ being Subset of X st ex Z being Subset of (LinearTopSpaceNorm X) st
( Z = Y & b₁ = Cl Z ) & ex Z being Subset of (LinearTopSpaceNorm X) st
( Z = Y & b₂ = Cl Z ) holds
b₁ = b₂ ) ) ; :: thesis: verum