environ
vocabularies HIDDEN, NUMBERS, REAL_1, SUBSET_1, RCOMP_1, SEQ_1, PARTFUN1, VALUED_0, SEQ_2, ORDINAL2, CARD_1, ARYTM_3, FUNCT_1, RELAT_1, FUNCOP_1, VALUED_1, FUNCT_2, NAT_1, TARSKI, ARYTM_1, XXREAL_1, XBOOLE_0, XXREAL_0, COMPLEX1, FCONT_1, XXREAL_2, FDIFF_1, FUNCT_7, ASYMPT_1, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, RELSET_1, PARTFUN1, PARTFUN2, RCOMP_1, FCONT_1, XXREAL_0;
definitions TARSKI, FCONT_1, XBOOLE_0, RCOMP_1, ORDINAL1;
theorems TARSKI, NAT_1, FUNCT_1, ABSVALUE, ZFMISC_1, SEQ_1, SEQ_2, SEQM_3, SEQ_4, PARTFUN1, PARTFUN2, RFUNCT_1, RFUNCT_2, RCOMP_1, FCONT_1, FUNCT_2, RELAT_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, FUNCOP_1, XREAL_1, COMPLEX1, VALUED_1, VALUED_0, ORDINAL1;
schemes SEQ_1;
registrations FUNCT_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, RCOMP_1, VALUED_0, VALUED_1, FUNCT_2, FUNCOP_1, SEQ_4, RELAT_1, SEQ_1, SEQ_2;
constructors HIDDEN, PARTFUN1, REAL_1, NAT_1, COMPLEX1, SEQ_2, SEQM_3, RCOMP_1, PARTFUN2, RFUNCT_2, FCONT_1, VALUED_1, REALSET1, FINSET_1, SETFAM_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, VALUED_1, RCOMP_1, SUBSET_1, ORDINAL1;
expansions TARSKI, XBOOLE_0, RCOMP_1;
set cs = seq_const 0;
reconsider cf = REAL --> (In (0,REAL)) as Function of REAL,REAL ;
reconsider j = 1 as Element of REAL by XREAL_0:def 1;
Lm1:
{} REAL is closed
by XBOOLE_1:3;
Lm2:
[#] REAL is open
by XBOOLE_1:37, Lm1;