environ
vocabularies HIDDEN, STRUCT_0, SETFAM_1, ZFMISC_1, CARD_3, TARSKI, NUMBERS, FUNCT_1, RELAT_1, CARD_1, ORDINAL1, SUBSET_1, XBOOLE_0, PRE_TOPC, TOPGEN_1, FINSET_1, WAYBEL23, RCOMP_1, RLVECT_3, TOPS_1, CONNSP_1, PCOMPS_1, NATTRA_1, PROB_1, MEASURE1, MCART_1, TOPMETR, CONNSP_2, WAYBEL30, OPENLATT, EQREL_1, NAT_1, TOPGEN_4;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, XFAMILY, SUBSET_1, RELAT_1, FUNCT_1, CARD_1, ORDINAL1, NUMBERS, CARD_3, MCART_1, WELLORD2, FINSET_1, SETFAM_1, DOMAIN_1, CONNSP_2, ZFMISC_1, STRUCT_0, OPENLATT, MEASURE1, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1, TDLAT_3, WAYBEL23, PROB_1, TOPMETR, CANTOR_1, ORDERS_4, TOPGEN_1, TOPGEN_3, PCOMPS_1;
definitions TARSKI, XBOOLE_0, CARD_3, MEASURE1;
theorems TARSKI, SETFAM_1, FUNCT_1, FUNCT_2, ZFMISC_1, PRE_TOPC, TOPS_1, XBOOLE_1, SUBSET_1, YELLOW_8, WAYBEL23, TOPMETR, NUMBERS, CONNSP_1, CONNSP_2, CARD_4, CARD_1, PCOMPS_1, XBOOLE_0, TOPGEN_1, TOPS_2, MEASURE1, WAYBEL12, MCART_1, TSP_1, TOPGEN_2, TOPGEN_3, PROB_1, CARD_2, TOPS_3, NAT_1, CARD_3;
schemes FUNCT_1, TREES_2, BORSUK_2, SUBSET_1, XFAMILY;
registrations SUBSET_1, RELSET_1, FINSET_1, NUMBERS, CARD_1, MEASURE1, STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_3, TOPMETR, TOPREAL6, TOPGEN_2, TOPGEN_1, CARD_3, COMPTS_1, XTUPLE_0;
constructors HIDDEN, MEASURE1, TOPS_1, CONNSP_1, COMPTS_1, TDLAT_3, TOPMETR, OPENLATT, WAYBEL23, TOPGEN_2, ORDERS_4, TOPGEN_1, TOPGEN_3, PCOMPS_1, XTUPLE_0, XFAMILY;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities XBOOLE_0, SUBSET_1, STRUCT_0, OPENLATT;
expansions TARSKI, XBOOLE_0, CARD_3, MEASURE1;
Lm1:
for X being set holds
( X is countable iff ex f being Function st
( dom f = RAT & X c= rng f ) )
by CARD_1:12, TOPGEN_3:17;
Lm2:
for T being set
for F being Subset-Family of T st F is SigmaField of T holds
F is closed_for_countable_unions