defpred S₁[ Element of REAL ] means 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 : V,Q is_dst v } is Subset of REAL ; :: thesis: verum