:: deftheorem defines null FOMODEL0:def 25 :
for x being set holds x null = x;