let L1, L2 be Subset of (the_Edges_of G); :: thesis: ( ( for e being object holds
( e in L1 iff ex v being object st e Joins v,v,G ) ) & ( for e being object holds
( e in L2 iff ex v being object st e Joins v,v,G ) ) implies L1 = L2 )
assume that
A3: for e being object holds
( e in L1 iff ex v being object st e Joins v,v,G ) and
A4: for e being object holds
( e in L2 iff ex v being object st e Joins v,v,G ) ; :: thesis: L1 = L2
for e being object holds
( e in L1 iff e in L2 )

proof

let e be object ; :: thesis: ( e in L1 iff e in L2 )

hereby :: thesis: ( e in L2 implies e in L1 )

assume e in L1 ; :: thesis: e in L2
then ex v being object st e Joins v,v,G by A3;
hence e in L2 by A4; :: thesis: verum

end;

assume e in L2 ; :: thesis: e in L1
then ex v being object st e Joins v,v,G by A4;
hence e in L1 by A3; :: thesis: verum

end;

hence L1 = L2 by TARSKI:2; :: thesis: verum