let G be VGraph; :: thesis: for v being Vertex of G
for x being set holds v in (G .labelVertex v,x) .labeledV()
let v be Vertex of G; :: thesis: for x being set holds v in (G .labelVertex v,x) .labeledV()
let x be set ; :: thesis: v in (G .labelVertex v,x) .labeledV()
A1: (G .labelVertex v,x) .labeledV() = (G .labeledV() ) \/ {v} by Th59;
v in {v} by TARSKI:def 1;
hence v in (G .labelVertex v,x) .labeledV() by A1, XBOOLE_0:def 3; :: thesis: verum