environ
vocabularies HIDDEN, NUMBERS, PRE_TOPC, SUBSET_1, ZFMISC_1, TEX_1, TDLAT_3, XBOOLE_0, STRUCT_0, TOPS_1, RCOMP_1, TARSKI, DECOMP_1, TOPMETR, XXREAL_1, XXREAL_0, BORSUK_5, ARYTM_3, LIMFUNC1, ISOMICHI, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XREAL_0, LIMFUNC1, RCOMP_1, NUMBERS, DOMAIN_1, ZFMISC_1, STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_3, TEX_1, TOPMETR, BORSUK_5, SEQ_4, DECOMP_1, XXREAL_0;
definitions TARSKI;
theorems SUBSET_1, XBOOLE_0, XBOOLE_1, PRE_TOPC, TOPS_1, TDLAT_1, TDLAT_3, PCOMPS_1, TEX_1, BORSUK_5, TOPMETR, DECOMP_1, TOPGEN_1, TOPS_3, XXREAL_0, XXREAL_1, JORDAN5A;
schemes ;
registrations XBOOLE_0, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, ZFMISC_1, STRUCT_0, TOPS_1, TEX_1, TEX_2, TOPMETR, FCONT_3, PRE_TOPC;
constructors HIDDEN, PROB_1, SEQ_4, RCOMP_1, LIMFUNC1, TOPS_1, TDLAT_3, TEX_1, TOPMETR, BORSUK_5, DECOMP_1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, REAL;
equalities SUBSET_1, STRUCT_0, LIMFUNC1, PROB_1;
expansions SUBSET_1;
Lm1:
for a, b being Real st a < b holds
[.a,b.] \/ {b} = [.a,b.]
:: A is condensed implies A` is condensed = TDLAT_1:16;