let G2 be _Graph; :: thesis: for v being object
for G1 being addVertex of G2,v holds v is Vertex of G1
let v be object ; :: thesis: for G1 being addVertex of G2,v holds v is Vertex of G1
let G1 be addVertex of G2,v; :: thesis: v is Vertex of G1
v in {v} by TARSKI:def 1;
hence v is Vertex of G1 by Th90; :: thesis: verum