environ
vocabularies HIDDEN, NUMBERS, REAL_1, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1, NAT_1, FDIFF_1, SUBSET_1, RELAT_1, RCOMP_1, TARSKI, SEQ_1, ARYTM_3, VALUED_1, FUNCT_2, ARYTM_1, SEQ_2, ORDINAL2, SUPINF_2, FCONT_1, COMPLEX1, STRUCT_0, CARD_1, VALUED_0, XXREAL_0, FUNCOP_1, XXREAL_2, XBOOLE_0, XXREAL_1, FUNCT_7, ASYMPT_1;
notations HIDDEN, TARSKI, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, VALUED_0, COMPLEX1, VALUED_1, SEQ_1, SEQ_2, RCOMP_1, FDIFF_1, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_0, NORMSP_1, NDIFF_1, NFCONT_3;
definitions RCOMP_1, XBOOLE_0, TARSKI;
theorems TARSKI, ABSVALUE, XBOOLE_0, XBOOLE_1, RLVECT_1, XCMPLX_0, XCMPLX_1, ZFMISC_1, SEQ_1, SEQ_2, NAT_1, RELAT_1, FUNCT_1, VFUNCT_1, FUNCT_2, ORDINAL1, SEQ_4, NORMSP_1, LOPBAN_1, LOPBAN_3, PARTFUN1, PARTFUN2, FDIFF_1, NDIFF_1, FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0, VALUED_1, VALUED_0, NORMSP_0, XREAL_0, RCOMP_1, SEQM_3, RFUNCT_2, NFCONT_3;
schemes FUNCT_2, SEQ_1;
registrations RELSET_1, STRUCT_0, ORDINAL1, XREAL_0, MEMBERED, FUNCT_2, NUMBERS, VALUED_0, NORMSP_0, NORMSP_1, RELAT_1, SUBSET_1, FUNCOP_1, NAT_1, RCOMP_1, VALUED_1, SEQ_4, FDIFF_1, SEQ_1, SEQ_2;
constructors HIDDEN, REAL_1, FDIFF_1, VFUNCT_1, NDIFF_1, RELSET_1, RVSUM_1, BINOP_2, INTEGR15, NAT_D, MEASURE6, NFCONT_3, COMSEQ_2, SEQ_1, NUMBERS;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities RCOMP_1, SUBSET_1, XBOOLE_0;
expansions RCOMP_1, XBOOLE_0, TARSKI;
set cs = seq_const 0;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
Lm1:
{} REAL is closed
;
Lm2:
[#] REAL is open
by XBOOLE_1:37, Lm1;