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

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

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

end;

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

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

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

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

end;

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

end;

end;