:: deftheorem defines size_w.r.t. PRELAMB:def 14 :
for s being non empty typealg
for b₂ being Function of the carrier of s,NAT holds
( b₂ = size_w.r.t. s iff for x being type of s holds b₂ . x = card (dom (repr_of x)) );