theorem Th2: :: ROUGHS_2:2

for R being non empty 1-sorted
for X being Subset of R holds { x where x is Element of R : {} c= X } = [#] R