environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, PROB_1, SETFAM_1, SUBSET_1, RPR_1, FUNCT_1, TARSKI, RELAT_1, REAL_1, CARD_1, ARYTM_1, CARD_3, PROB_3, NAT_1, ARYTM_3, ZFMISC_1, PROB_2, DYNKIN, VALUED_1, XXREAL_0, SERIES_1, ORDINAL2, FUNCOP_1, FINSEQ_1, FINSET_1, FINSUB_1, SETWISEO, ORDINAL4, EQREL_1, KOLMOG01;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REAL_1, ORDINAL1, XCMPLX_0, XXREAL_0, NAT_1, XREAL_0, NUMBERS, FINSET_1, DYNKIN, FINSUB_1, RELAT_1, CARD_3, SEQ_2, SETFAM_1, FUNCT_1, RELSET_1, VALUED_1, FINSEQ_1, RVSUM_1, PARTFUN1, FUNCT_2, PROB_3, SERIES_1, FUNCOP_1, SETWISEO, FINSEQOP, KURATO_0, PROB_1, PROB_2;
definitions TARSKI, XBOOLE_0;
theorems XCMPLX_1, PROB_1, TARSKI, SUBSET_1, XBOOLE_0, DYNKIN, ZFMISC_1, PROB_2, XBOOLE_1, SERIES_1, PROB_3, PROB_4, FUNCT_1, FUNCT_2, SEQ_1, SEQ_2, RELAT_1, SETFAM_1, CARD_5, FINSUB_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, RVSUM_1, ORDINAL1, WELLORD2, FINSEQOP, NAT_1, VALUED_0, FUNCOP_1, RELSET_1;
schemes NAT_1, XBOOLE_0, SETWISEO, PARTFUN1, FUNCT_2, XFAMILY;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, VALUED_1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, PROB_1, RELAT_1, FINSET_1, FINSEQ_1, FINSUB_1, FUNCT_1, FUNCT_2, VALUED_0, PROB_3;
constructors HIDDEN, SEQ_2, DYNKIN, REAL_1, PROB_3, SERIES_1, KURATO_0, RINFSUP1, SETFAM_1, BINOP_2, RVSUM_1, WELLORD2, FINSEQOP, SETWISEO, RELSET_1, MEASURE1, COMSEQ_2;
requirements HIDDEN, SUBSET, NUMERALS, BOOLE, ARITHM;
equalities PROB_1, SUBSET_1, XBOOLE_0, CARD_3;
expansions PROB_1, TARSKI, XBOOLE_0;
theorem Th2:
for
r being
Real holds
( not
r * r = r or
r = 0 or
r = 1 )