let X, Y be set ; :: thesis: for U being Grothendieck st X in Y & Y in U holds
X in U
let U be Grothendieck; :: thesis: ( X in Y & Y in U implies X in U )
assume ( X in Y & Y in U ) ; :: thesis: X in U
then ( union Y in U & X c= union Y ) by Def2, ZFMISC_1:74;
hence X in U by CLASSES1:def 1; :: thesis: verum