defpred S₁[ set ] means ex e being Element of the carrier' of G st
( e in X & ( $1 = the Source of G . e or $1 = the Target of G . e ) );
{ v where v is Vertex of G : S₁[v] } is Subset of the carrier of G from DOMAIN_1:sch 7();
hence G -VSet X is Subset of the carrier of G ; :: thesis: verum