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

suppose A5: S is empty ; :: thesis: ex b₁ being set st
for E being object holds
( E in b₁ iff ex G being _Graph st
( G in S & E = the_Edges_of G ) )

take the empty set ; :: thesis: for E being object holds
( E in the empty set iff ex G being _Graph st
( G in S & E = the_Edges_of G ) )
thus for E being object holds
( E in the empty set iff ex G being _Graph st
( G in S & E = the_Edges_of G ) ) by A5; :: thesis: verum

end;

suppose not S is empty ; :: thesis: ex b₁ being set st
for E being object holds
( E in b₁ iff ex G being _Graph st
( G in S & E = the_Edges_of G ) )

then reconsider S0 = S as non empty Graph-membered set ;
take X = { (the_Edges_of G) where G is Element of S0 : verum } ; :: thesis: for E being object holds
( E in X iff ex G being _Graph st
( G in S & E = the_Edges_of G ) )
let E be object ; :: thesis: ( E in X iff ex G being _Graph st
( G in S & E = the_Edges_of G ) )

hereby :: thesis: ( ex G being _Graph st
( G in S & E = the_Edges_of G ) implies E in X )

assume E in X ; :: thesis: ex G being _Graph st
( G in S & E = the_Edges_of G )
then consider G being Element of S0 such that
A6: E = the_Edges_of G ;
reconsider G = G as _Graph ;
take G = G; :: thesis: ( G in S & E = the_Edges_of G )
thus ( G in S & E = the_Edges_of G ) by A6; :: thesis: verum

end;

thus ( ex G being _Graph st
( G in S & E = the_Edges_of G ) implies E in X ) ; :: thesis: verum

end;

end;