:: deftheorem defines \ RANKNULL:def 3 :
for V being 1-sorted
for X being Subset of V holds V \ X = ([#] V) \ X;