set VT = { v where v is Vertex of G : ex i being Nat st
( i in dom pe & v in vertices (pe /. i) ) } ;
{ v where v is Vertex of G : ex i being Nat st
( i in dom pe & v in vertices (pe /. i) ) } c= the carrier of G

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Vertex of G : ex i being Nat st
( i in dom pe & v in vertices (pe /. i) ) } or x in the carrier of G )
assume x in { v where v is Vertex of G : ex i being Nat st
( i in dom pe & v in vertices (pe /. i) ) } ; :: thesis: x in the carrier of G
then ex v being Vertex of G st
( x = v & ex i being Nat st
( i in dom pe & v in vertices (pe /. i) ) ) ;
hence x in the carrier of G ; :: thesis: verum

end;

hence { v where v is Vertex of G : ex i being Nat st
( i in dom pe & v in vertices (pe /. i) ) } is Subset of the carrier of G ; :: thesis: verum