theorem Th14: :: CLASSES3:14

for X being set
for U being Grothendieck st X in U holds
Rrank X in U