theorem :: CLASSES3:12

for X being set
for A being Ordinal
for U being Grothendieck st X in U & X,A are_equipotent holds
A in U