environ
vocabularies HIDDEN, SUBSET_1, PRE_TOPC, SETFAM_1, STRUCT_0, TARSKI, FUNCT_2, ZFMISC_1, XBOOLE_0, FINSET_1, FUNCT_1, RELAT_1, RCOMP_1, FINSEQ_1, NAT_1, XXREAL_0, ARYTM_3, CARD_1, ORDINAL2, VALUED_1, RELAT_2, CONNSP_1, TOPS_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, XCMPLX_0, NAT_1, FINSEQ_1, FINSET_1, SETFAM_1, STRUCT_0, PRE_TOPC, CONNSP_1;
definitions TARSKI, PRE_TOPC;
theorems TARSKI, FINSET_1, SETFAM_1, FUNCT_1, FUNCT_2, FUNCT_3, NAT_1, FINSEQ_1, ZFMISC_1, PRE_TOPC, TOPS_1, RELAT_1, XBOOLE_0, XBOOLE_1, XREAL_1, CONNSP_1;
schemes CLASSES1, NAT_1, SUBSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, PRE_TOPC, XREAL_0, FINSEQ_1, RELAT_1, FUNCT_1, ORDINAL1, NAT_1;
constructors HIDDEN, SETFAM_1, PARTFUN1, FUNCT_3, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, CONNSP_1, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities SUBSET_1, STRUCT_0, RELAT_1;
expansions TARSKI, PRE_TOPC;
Lm1:
for T being 1-sorted
for F being Subset-Family of T st COMPLEMENT F is finite holds
F is finite
:: A FAMILY OF SETS IN TOPOLOGICAL SPACES
::