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