theorem Th13: :: CLASSES3:13

for X, Y being set
for U being Grothendieck st X in Y & Y in U holds
X in U