let G be Grothendieck; :: thesis: union G = G

per cases ( G is empty or not G is empty ) ;

suppose G is empty ; :: thesis: union G = G

hence union G = G by ZFMISC_1:2; :: thesis: verum

end;

suppose not G is empty ; :: thesis: union G = G

then reconsider G = G as non empty Grothendieck ;

now :: thesis: ( union G c= G & G c= union G )

now :: thesis: for o being object st o in union G holds
o in G

let o be object ; :: thesis: ( o in union G implies o in G )
assume o in union G ; :: thesis: o in G
then consider o9 being set such that
A1: ( o in o9 & o9 in G ) by TARSKI:def 4;
reconsider o9 = o9 as Element of G by A1;
G is axiom_GU1 ;
hence o in G by A1; :: thesis: verum

end;

hence union G c= G ; :: thesis: G c= union G

now :: thesis: for o being object st o in G holds
o in union G

let o be object ; :: thesis: ( o in G implies o in union G )
assume o in G ; :: thesis: o in union G
then reconsider o9 = o as Element of G ;
( o in {o9} & {o9} in G ) by TARSKI:def 1;
hence o in union G by TARSKI:def 4; :: thesis: verum

end;

hence G c= union G ; :: thesis: verum

end;

hence union G = G ; :: thesis: verum

end;

end;