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