environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, CQC_LANG, FINSEQ_1, ARYTM_3, XXREAL_0, TARSKI, CARD_1, XBOOLE_0, NAT_1, FINSET_1, RELAT_1, ORDINAL4, FUNCT_1, CALCUL_1, FUNCT_2, CQC_THE1, QC_LANG1, XBOOLEAN, FINSEQ_5, ARYTM_1, FINSEQ_2, CALCUL_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, CARD_1, NUMBERS, XXREAL_0, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, QC_LANG1, CQC_LANG, FINSET_1, FINSEQ_5, FINSEQ_2, RELSET_1, FUNCT_2, WELLORD2, CALCUL_1;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, FINSEQ_1, FINSEQ_3, FUNCT_1, XBOOLE_0, FINSEQ_2, RELAT_1, NAT_1, XBOOLE_1, FUNCT_2, CALCUL_1, QC_LANG2, CARD_1, ORDINAL1, FUNCT_4, FINSEQ_5, INT_1, XREAL_1, XXREAL_0, FUNCOP_1, AFINSQ_1;
schemes NAT_1, RECDEF_1;
registrations FUNCT_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, CQC_LANG, FUNCT_2, FINSEQ_2, CARD_1;
constructors HIDDEN, PARTFUN1, WELLORD2, XXREAL_0, REAL_1, NAT_1, INT_1, FINSEQ_2, FINSEQ_5, CALCUL_1, RELSET_1, QC_LANG1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, FINSEQ_2, CARD_1, ORDINAL1;
expansions TARSKI;
theorem Th1:
for
a,
b,
c being
Nat holds
(
c in seq (
a,
b) iff ( 1
+ a <= c &
c <= b + a ) )
theorem Th3:
for
a,
b being
Nat holds
(
b = 0 or
b + a in seq (
a,
b) )
theorem Th4:
for
a,
b1,
b2 being
Nat holds
(
b1 <= b2 iff
seq (
a,
b1)
c= seq (
a,
b2) )