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