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()
( (G .labelVertex (v,x)) .labeledV() = (G .labeledV()) \/ {v} & v in {v} ) by Th52, TARSKI:def 1;
hence v in (G .labelVertex (v,x)) .labeledV() by XBOOLE_0:def 3; :: thesis: verum