environ
vocabularies HIDDEN, NUMBERS, REAL_1, XXREAL_0, CARD_1, SUBSET_1, ARYTM_3, XBOOLE_0, STRUCT_0, NAT_1, RELAT_1, TARSKI, PRE_TOPC, RLVECT_3, RCOMP_1, SETFAM_1, FUNCT_1, ZFMISC_1, METRIC_1, XXREAL_1, ARYTM_1, COMPLEX1, TOPMETR, PCOMPS_1, ORDINAL1, CARD_3, FUNCT_4, FUNCOP_1, SEQ_2, PARTFUN1, FRECHET, YELLOW_8;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, SETFAM_1, RELAT_1, FUNCT_1, PARTFUN1, RELSET_1, FUNCT_2, BINOP_1, FUNCOP_1, STRUCT_0, CARD_3, FUNCT_4, RCOMP_1, PRE_TOPC, TOPS_2, METRIC_1, PCOMPS_1, TOPMETR, YELLOW_8, XXREAL_0;
definitions TARSKI, TOPS_2, XBOOLE_0;
theorems TARSKI, ZFMISC_1, SUBSET_1, SETFAM_1, PRE_TOPC, FUNCT_1, FUNCT_2, FUNCT_4, FUNCOP_1, NORMSP_1, NAT_1, ORDINAL1, RELAT_1, YELLOW_8, TOPS_1, TOPS_2, TOPMETR, RCOMP_1, METRIC_1, PCOMPS_1, GOBOARD6, RELSET_1, XREAL_0, XBOOLE_0, XBOOLE_1, SEQ_4, COMPLEX1, XREAL_1, XXREAL_0, CARD_3, NUMBERS;
schemes DOMAIN_1, CLASSES1, NAT_1, CARD_4, FUNCT_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, PCOMPS_1, TOPMETR, RELSET_1;
constructors HIDDEN, FUNCT_4, REAL_1, NAT_1, MEMBERED, COMPLEX1, RCOMP_1, PCOMPS_1, FUNCOP_1, CARD_3, TOPS_2, TOPMETR, YELLOW_8, BINOP_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities SUBSET_1, STRUCT_0, RELAT_1, XCMPLX_0, TOPMETR, CARD_1, ORDINAL1;
expansions TARSKI, TOPS_2, XBOOLE_0;
Lm1:
for r being Real st r > 0 holds
ex n being Nat st
( 1 / n < r & n > 0 )
Lm2:
for T being TopStruct
for A being Subset of T holds
( A is open iff ([#] T) \ A is closed )
theorem Th13:
for
A,
B being
set st
B c= A holds
(id A) .: B = B
Lm3:
{REAL} c= the carrier of REAL?
:: Preliminaries
::