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