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