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