suppose e in the_Edges_of G ; :: thesis:

then G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Def21;
hence G .labelEdge (e,x) is [VLabeled] ; :: thesis:

end;

suppose not e in the_Edges_of G ; :: thesis:

hence G .labelEdge (e,x) is [VLabeled] by Def21; :: thesis:

end;

end;

end;

hence G .labelEdge (e,x) is [VLabeled] ; :: thesis: