:: deftheorem defClN defines ClNLin NORMSP_3:def 20 :
for X being RealNormSpace
for Y being Subset of X
for b₃ being non empty NORMSTR holds
( b₃ = ClNLin Y iff ex Z being Subset of X st
( Z = the carrier of (Lin Y) & b₃ = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) );