defpred S₁[ Element of M -neighbour ] means ex Q being Element of M -neighbour ex v being Element of REAL st $1,Q is_dst v;
{ V where V is Element of M -neighbour : S₁[V] } c= M -neighbour from FRAENKEL:sch 10();
hence { V where V is Element of M -neighbour : ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v } is Subset of ; :: thesis: verum