theorem :: DOMAIN_1:18

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