theorem Th1: :: CLASSES4:1

for X being set holds
( proj1 X in bool (union (union X)) & proj2 X in bool (union (union X)) )