:: deftheorem defines DOM CARD_3:def 11 :
for X being functional set holds DOM X = meet { (dom f) where f is Element of X : verum } ;