let E1, E2 be Subset of (the_Vertices_of G); :: thesis: ( ( for v being object holds
( v in E1 iff ex w being Vertex of G st
( v = w & w is endvertex ) ) ) & ( for v being object holds
( v in E2 iff ex w being Vertex of G st
( v = w & w is endvertex ) ) ) implies E1 = E2 )
assume that
A2: for v being object holds
( v in E1 iff ex w being Vertex of G st
( v = w & w is endvertex ) ) and
A3: for v being object holds
( v in E2 iff ex w being Vertex of G st
( v = w & w is endvertex ) ) ; :: thesis: E1 = E2

now :: thesis: for v being object holds
( ( v in E1 implies v in E2 ) & ( v in E2 implies v in E1 ) )

let v be object ; :: thesis: ( ( v in E1 implies v in E2 ) & ( v in E2 implies v in E1 ) )

hereby :: thesis: ( v in E2 implies v in E1 )

assume v in E1 ; :: thesis: v in E2
then ex w being Vertex of G st
( v = w & w is endvertex ) by A2;
hence v in E2 by A3; :: thesis: verum

end;

assume v in E2 ; :: thesis: v in E1
then ex w being Vertex of G st
( v = w & w is endvertex ) by A3;
hence v in E1 by A2; :: thesis: verum

end;

hence E1 = E2 by TARSKI:2; :: thesis: verum