theorem Th17: :: CLASSES3:17

for U being Grothendieck holds U is Tarski