let IT1, IT2 be Subset of (the_Edges_of G); :: thesis: ( ( for e being set holds
( e in IT1 iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) ) & ( for e being set holds
( e in IT2 iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) ) implies IT1 = IT2 )
assume that
A7: for e being set holds
( e in IT1 iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) and
A8: for e being set holds
( e in IT2 iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) ; :: thesis: IT1 = IT2
now :: thesis: for e being object holds
( ( e in IT1 implies e in IT2 ) & ( e in IT2 implies e in IT1 ) )
let e be object ; :: thesis: ( ( e in IT1 implies e in IT2 ) & ( e in IT2 implies e in IT1 ) )
hereby :: thesis: ( e in IT2 implies e in IT1 )
assume A9: e in IT1 ; :: thesis: e in IT2
then (the_Source_of G) . e in X by A7;
hence e in IT2 by A8, A9; :: thesis: verum
end;
assume A10: e in IT2 ; :: thesis: e in IT1
then (the_Source_of G) . e in X by A8;
hence e in IT1 by A7, A10; :: thesis: verum
end;
hence IT1 = IT2 by TARSKI:2; :: thesis: verum