let X be set ; :: thesis: ( X = the_Edges_of S iff X = { (the_Edges_of G) where G is Element of S : verum } )
set Y = { (the_Edges_of G) where G is Element of S : verum } ;
now :: thesis: for E being object holds
( ( E in the_Edges_of S implies E in { (the_Edges_of G) where G is Element of S : verum } ) & ( E in { (the_Edges_of G) where G is Element of S : verum } implies E in the_Edges_of S ) )
let E be object ; :: thesis: ( ( E in the_Edges_of S implies E in { (the_Edges_of G) where G is Element of S : verum } ) & ( E in { (the_Edges_of G) where G is Element of S : verum } implies E in the_Edges_of S ) )
hereby :: thesis: ( E in { (the_Edges_of G) where G is Element of S : verum } implies E in the_Edges_of S )
assume E in the_Edges_of S ; :: thesis: E in { (the_Edges_of G) where G is Element of S : verum }
then ex G being _Graph st
( G in S & E = the_Edges_of G ) by Def15;
hence E in { (the_Edges_of G) where G is Element of S : verum } ; :: thesis: verum
end;
assume E in { (the_Edges_of G) where G is Element of S : verum } ; :: thesis: E in the_Edges_of S
then consider G being Element of S such that
A2: E = the_Edges_of G ;
thus E in the_Edges_of S by A2, Def15; :: thesis: verum
end;
hence ( X = the_Edges_of S iff X = { (the_Edges_of G) where G is Element of S : verum } ) by TARSKI:2; :: thesis: verum