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