environ
vocabularies HIDDEN, XBOOLE_0, PRE_TOPC, SUBSET_1, STRUCT_0, CARD_3, CARD_1, TARSKI, ORDINAL1, FINSET_1, NATTRA_1, TOPS_1, SETFAM_1, RCOMP_1, RLVECT_3, GLIB_000, TOPMETR, NUMBERS, BORSUK_5, TOPGEN_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, CARD_1, ORDINAL1, NUMBERS, CARD_3, FINSET_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_3, YELLOW_8, TOPMETR, BORSUK_5, ORDERS_4;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, ZFMISC_1, PRE_TOPC, TOPS_1, XBOOLE_0, XBOOLE_1, SUBSET_1, TOPS_3, TDLAT_3, YELLOW_8, FRECHET, BORSUK_5, TOPMETR, NUMBERS, CARD_4, ORDERS_4, CARD_3;
schemes ORDINAL1, SUBSET_1;
registrations SUBSET_1, CARD_1, STRUCT_0, TOPS_1, TEX_1, TEX_4, YELLOW13, TOPMETR;
constructors HIDDEN, CARD_3, TOPS_1, TDLAT_3, TOPMETR, YELLOW_8, BORSUK_5, ORDERS_4, TOPS_2;
requirements HIDDEN, BOOLE, SUBSET;
equalities XBOOLE_0, SUBSET_1, STRUCT_0;
expansions TARSKI, XBOOLE_0;
Lm1:
for T being TopSpace
for A being Subset of T st A is closed & A is dense-in-itself holds
Der A = A
Lm2:
RAT = REAL \ IRRAT
reconsider B = RAT as Subset of R^1 by NUMBERS:12, TOPMETR:17;
reconsider A = IRRAT as Subset of R^1 by TOPMETR:17;