:: deftheorem Def4 defines Grothendieck CLASSES3:def 4 :
for X being set
for b₂ being Grothendieck holds
( b₂ is Grothendieck of X iff X in b₂ );