let a be real number ; :: thesis: ].a,+infty.[ <> REAL
a in REAL by XREAL_0:def 1;
hence ].a,+infty.[ <> REAL by XXREAL_1:235; :: thesis: verum