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 )

( 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

hence
L1 = L2
by TARSKI:2; :: thesis: verum
let e be object ; :: thesis: ( e in L1 iff e in L2 )

then ex v being object st e Joins v,v,G by A4;

hence e in L1 by A3; :: thesis: verum

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

assume
e in L2
; :: thesis: e in L1assume
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;then ex v being object st e Joins v,v,G by A3;

hence e in L2 by A4; :: thesis: verum

then ex v being object st e Joins v,v,G by A4;

hence e in L1 by A3; :: thesis: verum