now

per cases ( e in the_Edges_of G or not e in the_Edges_of G ) ;

suppose e in the_Edges_of G ; :: thesis: not G .labelEdge e,x is trivial

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

end;

suppose not e in the_Edges_of G ; :: thesis: not G .labelEdge e,x is trivial

hence not G .labelEdge e,x is trivial by Def21; :: thesis: verum

end;

end;

end;

hence not G .labelEdge e,x is trivial ; :: thesis: verum