theorem Th72: :: CARD_3:72

for X being functional with_common_domain set st X = {{}} holds
DOM X = {}