let G be EGraph; :: thesis: for e, x being set st e in the_Edges_of G holds
G .labeledE() c= (G .labelEdge (e,x)) .labeledE()
let e, x be set ; :: thesis: ( e in the_Edges_of G implies G .labeledE() c= (G .labelEdge (e,x)) .labeledE() )
assume e in the_Edges_of G ; :: thesis: G .labeledE() c= (G .labelEdge (e,x)) .labeledE()
then (G .labelEdge (e,x)) .labeledE() = (G .labeledE()) \/ {e} by Th45;
hence G .labeledE() c= (G .labelEdge (e,x)) .labeledE() by XBOOLE_1:7; :: thesis: verum