let G be EGraph; :: thesis: for e, x being set st e in the_Edges_of G holds
e in (G .labelEdge (e,x)) .labeledE()
let e, x be set ; :: thesis: ( e in the_Edges_of G implies e in (G .labelEdge (e,x)) .labeledE() )
assume e in the_Edges_of G ; :: thesis: e in (G .labelEdge (e,x)) .labeledE()
then A1: (G .labelEdge (e,x)) .labeledE() = (G .labeledE()) \/ {e} by Th45;
e in {e} by TARSKI:def 1;
hence e in (G .labelEdge (e,x)) .labeledE() by A1, XBOOLE_0:def 3; :: thesis: verum