begin
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 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
abs (d - c) < b - a
begin