let IT1, IT2 be Subset of (the_Edges_of G); :: thesis: ( ( for e being object holds
( e in IT1 iff e SJoins X,Y,G ) ) & ( for e being object holds
( e in IT2 iff e SJoins X,Y,G ) ) implies IT1 = IT2 )
assume that
A3: for e being object holds
( e in IT1 iff e SJoins X,Y,G ) and
A4: for e being object holds
( e in IT2 iff e SJoins X,Y,G ) ; :: thesis: IT1 = IT2
for e being object holds
( e in IT2 iff e in IT1 ) by A3, A4;
hence IT1 = IT2 by TARSKI:2; :: thesis: verum