q in REAL by XREAL_0:def 1;
then ].p,q.] c= REAL by Th227;
hence ].p,q.] is real-membered ; :: thesis: verum