environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, FINSEQ_1, TARSKI, FINSET_1, RELAT_1, CARD_1, ARYTM_3, XXREAL_0, REAL_1, ARYTM_1, RPR_1, BSPACE;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, DOMAIN_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, REAL_1, XREAL_0, FINSEQ_1, FINSET_1, XXREAL_0;
definitions XBOOLE_0;
theorems TARSKI, SUBSET_1, ZFMISC_1, FINSEQ_1, CARD_1, CARD_2, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, NAT_1;
schemes ;
registrations RELSET_1, FINSET_1, XXREAL_0, XREAL_0, CARD_1, ORDINAL1;
constructors HIDDEN, XXREAL_0, REAL_1, NAT_1, MEMBERED, FINSEQ_1, DOMAIN_1, XREAL_0;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, SUBSET_1;
expansions XBOOLE_0;
Lm1:
for E being non empty finite set holds 0 < card E