environ
vocabularies HIDDEN, NUMBERS, REAL_1, FINSEQ_1, VALUED_0, XBOOLE_0, NEWTON, ARYTM_3, RELAT_1, NAT_1, XXREAL_0, ARYTM_1, SUBSET_1, CARD_1, CARD_3, ORDINAL4, TARSKI, INT_2, FUNCT_1, FINSEQ_2, PRE_POLY, PBOOLE, FINSET_1, XCMPLX_0, UPROOTS, FUNCT_2, BINOP_2, SETWISEO, INT_1, FUNCOP_1, NAT_3, XREAL_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_D, INT_2, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, VALUED_0, PBOOLE, RVSUM_1, NEWTON, WSIERP_1, TREES_4, BINOP_2, FUNCOP_1, XXREAL_2, SETWOP_2, PRE_POLY;
definitions TARSKI, XBOOLE_0, INT_2, NAT_D, FINSEQ_1, VALUED_0, PRE_POLY;
theorems ORDINAL1, NEWTON, NAT_1, XCMPLX_1, INT_1, CARD_4, XREAL_0, RVSUM_1, INT_2, PEPIN, FUNCT_1, CARD_2, PREPOWER, FINSEQ_1, TARSKI, XBOOLE_1, FUNCOP_1, WSIERP_1, XBOOLE_0, FINSEQ_2, FINSEQ_3, FINSEQ_4, RELAT_1, FINSOP_1, FUNCT_2, XREAL_1, XXREAL_0, NAT_D, VALUED_0, XXREAL_2, PARTFUN1, PRE_POLY, CARD_1;
schemes NAT_1, PRE_CIRC, FINSEQ_1, FINSEQ_2, PBOOLE, CLASSES1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, BINOP_2, MEMBERED, NEWTON, VALUED_0, FINSEQ_1, XXREAL_2, CARD_1, FUNCT_2, RELSET_1, ZFMISC_1, FINSEQ_2, PRE_POLY, XREAL_0, RVSUM_1;
constructors HIDDEN, BINOP_1, SETWISEO, NAT_D, FINSEQOP, FINSOP_1, NEWTON, WSIERP_1, BINOP_2, XXREAL_2, RELSET_1, PRE_POLY, REAL_1;
requirements HIDDEN, NUMERALS, SUBSET, ARITHM, REAL, BOOLE;
equalities FINSEQ_1, FINSEQ_2, PBOOLE, ORDINAL1;
expansions TARSKI, XBOOLE_0, INT_2, NAT_D, FINSEQ_1, VALUED_0, PBOOLE;
theorem Th2:
for
a,
b being
Nat st 1
< a holds
b <= a |^ b