theorem :: DOMAIN_1:26

for X1 being non empty set holds {} X1 = { x1 where x1 is Element of X1 : contradiction }