theorem Th73: :: CLASSES4:73

for X being set
for U1 being Universe st U1 in Tarski-Class X holds
Tarski-Class U1 c= Tarski-Class X