environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, CARD_1, RELAT_1, MEMBER_1, TARSKI, ARYTM_3, XBOOLE_0, SUPINF_1, XXREAL_0, MEASURE5, XXREAL_1, ORDINAL2, XXREAL_2, MEMBERED, SEQ_4, ARYTM_1, NEWTON, INT_1, URYSOHN1, CARD_3, PROB_1, LIMFUNC1, NAT_1, COMPLEX1, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XXREAL_0, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NUMBERS, MEMBERED, MEMBER_1, NEWTON, INT_1, NAT_1, XXREAL_1, XXREAL_2, SUPINF_1, MEASURE5, PROB_1, URYSOHN1, INTEGRA2, LIMFUNC1, SEQ_4, SUPINF_2, EXTREAL1;
definitions TARSKI, XBOOLE_0, XXREAL_2;
theorems TARSKI, NAT_1, SEQ_4, ABSVALUE, URYSOHN1, XREAL_0, MEASURE5, MEASURE6, INT_1, INTEGRA2, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, NEWTON, XXREAL_1, MEMBERED, XXREAL_2, EXTREAL1, XXREAL_3, MEMBER_1;
schemes NAT_1;
registrations XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, XXREAL_1, SEQ_4, XXREAL_2, XXREAL_3, MEASURE5, MEMBER_1, NEWTON, ORDINAL1;
constructors HIDDEN, DOMAIN_1, REAL_1, NAT_1, PROB_1, LIMFUNC1, NEWTON, SUPINF_2, URYSOHN1, INTEGRA2, SUPINF_1, EXTREAL1, SEQ_4, PSCOMP_1, MEASURE5, BINOP_2;
requirements HIDDEN, NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
equalities PROB_1, LIMFUNC1, XCMPLX_0;
expansions TARSKI, XBOOLE_0;
Lm1:
for A being non empty Subset of REAL
for x being Real st x > 0 & x ** A is bounded_above holds
A is bounded_above
Lm2:
for A being non empty Subset of REAL
for x being Real st x > 0 & x ** A is bounded_below holds
A is bounded_below
theorem Th21:
for
eps being
Real st
0 < eps holds
ex
n being
Nat st 1
< (2 |^ n) * eps
theorem Th22:
for
a,
b being
Real st
0 <= a & 1
< b - a holds
ex
n being
Nat st
(
a < n &
n < b )
theorem Th25:
for
a,
b being
Real st
a < b holds
ex
c being
Real st
(
c in DOM &
a < c &
c < b )
theorem Th30:
for
a,
b,
c,
d being
Real st
a < c &
c < b &
a < d &
d < b holds
|.(d - c).| < b - a