set A = { x where x is Element of Vertices G : {v,x} in Edges G } ;
{ x where x is Element of Vertices G : {v,x} in Edges G } c= Vertices G

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { x where x is Element of Vertices G : {v,x} in Edges G } or a in Vertices G )
assume a in { x where x is Element of Vertices G : {v,x} in Edges G } ; :: thesis: a in Vertices G
then consider x being Element of Vertices G such that
A1: a = x and
A2: {v,x} in Edges G ;
thus a in Vertices G by A1, A2, Th13; :: thesis: verum

end;

then reconsider A = { x where x is Element of Vertices G : {v,x} in Edges G } as Subset of (Vertices G) ;
take A ; :: thesis: for x being Element of Vertices G holds
( x in A iff {v,x} in Edges G )
let x be Element of Vertices G; :: thesis: ( x in A iff {v,x} in Edges G )

hereby :: thesis: ( {v,x} in Edges G implies x in A )

assume x in A ; :: thesis: {v,x} in Edges G
then consider a being Element of Vertices G such that
A3: x = a and
A4: {v,a} in Edges G ;
thus {v,x} in Edges G by A3, A4; :: thesis: verum

end;

thus ( {v,x} in Edges G implies x in A ) ; :: thesis: verum