now

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

suppose v in the_Vertices_of G ; :: thesis: not G .labelVertex v,x is trivial

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

end;

suppose not v in the_Vertices_of G ; :: thesis: not G .labelVertex v,x is trivial

hence not G .labelVertex v,x is trivial by Def22; :: thesis: verum

end;

end;

end;

hence not G .labelVertex v,x is trivial ; :: thesis: verum