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

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