now :: thesis: G .labelVertex (v,x) is nonnegative-weighted

per cases ( v in the_Vertices_of G or not v in the_Vertices_of G ) ;

suppose v in the_Vertices_of G ; :: thesis: G .labelVertex (v,x) is nonnegative-weighted

then G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) by Def22;
hence G .labelVertex (v,x) is nonnegative-weighted ; :: thesis: verum

end;

suppose not v in the_Vertices_of G ; :: thesis: G .labelVertex (v,x) is nonnegative-weighted

hence G .labelVertex (v,x) is nonnegative-weighted by Def22; :: thesis: verum

end;

end;

end;

hence G .labelVertex (v,x) is nonnegative-weighted ; :: thesis: verum