:: deftheorem defines -null FOMODEL4:def 19 :
for S being Language
for x being set holds
( x is S -null iff verum );