for R being 1-sorted
for X being Subset of R holds { x where x is Element of R : {} meets X } = {} R