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_{1} being Subset of X ex Z being Subset of (LinearTopSpaceNorm X) st

( Z = Y & b_{1} = Cl Z ) & ( for b_{1}, b_{2} being Subset of X st ex Z being Subset of (LinearTopSpaceNorm X) st

( Z = Y & b_{1} = Cl Z ) & ex Z being Subset of (LinearTopSpaceNorm X) st

( Z = Y & b_{2} = Cl Z ) holds

b_{1} = b_{2} ) )
; :: thesis: verum

Cl Z is Subset of X by NORMSP_2:def 4;

hence ( ex b

( Z = Y & b

( Z = Y & b

( Z = Y & b

b