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