let X be set ; :: thesis: ( ( for Y being object st Y in X holds
Y is Graph-membered set ) implies union X is Graph-membered )
assume A1: for Y being object st Y in X holds
Y is Graph-membered set ; :: thesis: union X is Graph-membered
let x be object ; :: according to GLIB_014:def 1 :: thesis: ( x in union X implies x is _Graph )
assume x in union X ; :: thesis: x is _Graph
then consider Y being set such that
A2: ( x in Y & Y in X ) by TARSKI:def 4;
thus x is _Graph by A1, A2, Def1; :: thesis: verum