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