environ
vocabularies HIDDEN, XBOOLE_0, PROB_1, SUBSET_1, SETFAM_1, NUMBERS, RELAT_1, FUNCT_1, FINSET_1, ARYTM_3, CARD_1, FUNCT_7, CARD_3, TARSKI, ZFMISC_1, PROB_2, XXREAL_0, NAT_1, EQREL_1, DYNKIN, FINSUB_1;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, FINSET_1, CARD_1, ORDINAL1, NUMBERS, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, XCMPLX_0, NAT_1, FUNCT_7, CARD_3, PROB_1, FINSUB_1, PROB_2, XXREAL_0;
definitions TARSKI;
theorems TARSKI, FUNCT_1, ZFMISC_1, FUNCT_2, SUBSET_1, NAT_1, RELAT_1, SETFAM_1, PROB_2, FINSUB_1, XBOOLE_0, XBOOLE_1, PROB_1, ORDINAL1, XXREAL_0, FUNCT_7, MEASURE1;
schemes FUNCT_2, NAT_1, FINSET_1, XFAMILY;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FINSET_1, XREAL_0, FUNCT_7, CARD_1;
constructors HIDDEN, SETFAM_1, FINSUB_1, NAT_1, PROB_2, XREAL_0, FUNCT_7, ENUMSET1, RELSET_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities SUBSET_1, CARD_1, CARD_3, ORDINAL1;
expansions TARSKI;
Lm1:
for X being non empty set
for a, b, c being Element of X holds (a,b) followed_by c is sequence of X
;