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