theorem Th23: :: WAYBEL28:23

for X, Y being set st X c= Y holds
X in the_universe_of Y