theorem Th36: :: CLASSES4:36

for UN being Universe
for X being Element of UN holds
( proj1 X is Element of UN & proj2 X is Element of UN )