theorem Th1: :: XREGULAR:1

for X being non empty set ex Y being set st
( Y in X & Y misses X )