environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, FINSEQ_1, FUNCT_1, XXREAL_0, ORDINAL4, RELAT_1, TREES_1, XBOOLE_0, FINSET_1, TARSKI, TREES_2, FUNCT_2, CARD_1, ZFMISC_1, MCART_1, NAT_1, ARYTM_3, TREES_A, ARYTM_1, TREES_3, REAL_1, BINTREE1, ORDINAL1, TREES_4, HUFFMAN1, PROB_1, RANDOM_1, UPROOTS;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, DOMAIN_1, FUNCOP_1, FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, VALUED_0, XXREAL_2, FINSEQ_1, TREES_1, RVSUM_1, TREES_2, TREES_3, TREES_4, PROB_1, BINTREE1, RANDOM_1;
definitions TARSKI, XBOOLE_0, FUNCT_1;
theorems TARSKI, ZFMISC_1, FINSEQ_1, NAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSEQ_2, TREES_1, TREES_2, RELAT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, TREES_4, ORDINAL1, CARD_1, FINSET_1, TREES_3, XREAL_0, BINTREE1, CARD_2, XXREAL_2, WELLORD2, FINSEQ_3;
schemes NAT_1, XBOOLE_0, FINSEQ_1, RECDEF_1, FUNCT_2, FRAENKEL;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, TREES_3, FINSET_1, XREAL_0, NAT_1, FINSEQ_1, TREES_1, TREES_2, CARD_1, RELSET_1, MEMBERED, BINTREE1, XTUPLE_0, VALUED_0, RVSUM_1, NUMBERS, FRAENKEL, XXREAL_2, FUNCOP_1, TREES_4;
constructors HIDDEN, DOMAIN_1, XXREAL_2, RELSET_1, WELLORD2, BINTREE1, RVSUM_1, RANDOM_1, ARYTM_1, TREES_4, RFINSEQ2;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities TREES_2, TREES_3, TREES_4;
expansions BINTREE1;
defpred S1[ non empty finite Subset of (BinFinTrees IndexedREAL), finite binary DecoratedTree of IndexedREAL ] means ( $2 in $1 & ( for q being finite binary DecoratedTree of IndexedREAL st q in $1 holds
Vrootr $2 <= Vrootr q ) );
Lm1:
for X being set
for x being object st ex u, v being object st
( u <> v & u in X & v in X ) holds
X \ {x} <> {}
Lm2:
for X, Y being set
for t, s, z being object st X c= Y & t in Y & s in Y & z in Y holds
(X \ {t,s}) \/ {z} c= Y
Lm3:
for X being finite set st 2 <= card X holds
ex u, v being object st
( u <> v & u in X & v in X )
Lm4:
for X being finite set st 1 = card X holds
ex u being object st X = {u}
Lm5:
for X being finite set
for t, s, z being object st t in X & s in X & t <> s & not z in X holds
card ((X \ {t,s}) \/ {z}) = (card X) - 1