now

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

suppose A1: e in the_Edges_of G ; :: thesis: G .labelEdge (e,x) is real-elabeled

set EL = (the_ELabel_of G) +* (e .--> x);
rng (the_ELabel_of G) c= REAL ;
then the_ELabel_of G is PartFunc of (dom (the_ELabel_of G)),REAL by RELSET_1:11;
then the_ELabel_of G is PartFunc of (the_Edges_of G),REAL by Lm1, RELSET_1:13;
then reconsider EL = (the_ELabel_of G) +* (e .--> x) as PartFunc of (the_Edges_of G),REAL by A1, Lm4;
G .labelEdge (e,x) = G .set (ELabelSelector,EL) by A1, Def21;
hence G .labelEdge (e,x) is real-elabeled ; :: thesis: verum

end;

suppose not e in the_Edges_of G ; :: thesis: G .labelEdge (e,x) is real-elabeled

hence G .labelEdge (e,x) is real-elabeled by Def21; :: thesis: verum

end;

end;

end;

hence G .labelEdge (e,x) is real-elabeled ; :: thesis: verum