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