environ
vocabularies HIDDEN, NUMBERS, ORDINAL1, ORDINAL2, TARSKI, MATROID0, XBOOLE_0, CARD_1, FINSET_1, AFINSQ_1, ORDINAL4, RELAT_1, FUNCT_1, VALUED_0, CARD_3, SUBSET_1, ARYTM_3, NAT_1, XXREAL_0, NEWTON, ORDINAL3, FINSEQ_1, ORDINAL5;
notations HIDDEN, XBOOLE_0, TARSKI, RELAT_1, FUNCT_1, SUBSET_1, FINSET_1, ORDINAL1, XCMPLX_0, NAT_1, XXREAL_0, NEWTON, ORDINAL2, AFINSQ_1, ORDINAL3, ORDINAL4, CARD_1, CARD_3, NUMBERS;
definitions TARSKI, XBOOLE_0, ORDINAL2, ORDINAL1;
theorems TARSKI, FUNCT_1, FINSET_1, NAT_1, ORDERS_1, AFINSQ_1, RELAT_1, ORDINAL1, ORDINAL2, ORDINAL3, ORDINAL4, CARD_2, CARD_3, CARD_5, XBOOLE_0, XBOOLE_1, ZFMISC_1, NEWTON, XXREAL_0, NAT_4, PEPIN, XREGULAR;
schemes NAT_1, ORDINAL1, ORDINAL2, AFINSQ_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, NAT_1, XREAL_0, ORDINAL2, ORDINAL4, CARD_1, CARD_5, CARD_LAR, NEWTON, AFINSQ_1, FINSET_1;
constructors HIDDEN, NEWTON, NAT_1, AFINSQ_1, ORDINAL3, CARD_3, NUMBERS;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
equalities ORDINAL2, CARD_3, ORDINAL1, CARD_1;
expansions TARSKI, XBOOLE_0;
theorem Th28:
for
n,
k being
Nat st
n > 1 holds
n |^|^ k > k
Lm1:
0 in Segm 1
by NAT_1:44;
:: 1 in c & a in b implies c |^|^ a in c |^|^ b