defpred S₁[ Element of ] means $1 is_between p,r;
{ q where q is Element of : S₁[q] } c= the carrier of M from FRAENKEL:sch 10();
hence { q where q is Element of : q is_between p,r } is Subset of ; :: thesis: verum