([#] REAL) ` = {} REAL by XBOOLE_1:37;
hence [#] REAL is open by Lm1, RCOMP_1:def 5; :: thesis: verum