defpred S_{1}[ Element of M] means $1 is_between p,r;

A1: {p,r} c= the carrier of M by ZFMISC_1:32;

{ q where q is Element of M : S_{1}[q] } c= the carrier of M
from FRAENKEL:sch 10();

hence { q where q is Element of M : q is_between p,r } \/ {p,r} is Subset of M by A1, XBOOLE_1:8; :: thesis: verum

A1: {p,r} c= the carrier of M by ZFMISC_1:32;

{ q where q is Element of M : S

hence { q where q is Element of M : q is_between p,r } \/ {p,r} is Subset of M by A1, XBOOLE_1:8; :: thesis: verum