begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
scheme
RSetEq{
P1[
set ] } :
for
X1,
X2 being
Subset of
REAL st ( for
x being
R_eal holds
(
x in X1 iff
P1[
x] ) ) & ( for
x being
R_eal holds
(
x in X2 iff
P1[
x] ) ) holds
X1 = X2
:: deftheorem MEASURE5:def 1 :
canceled;
:: deftheorem defines ]. MEASURE5:def 2 :
:: deftheorem MEASURE5:def 3 :
canceled;
:: deftheorem MEASURE5:def 4 :
canceled;
:: deftheorem Def5 defines open_interval MEASURE5:def 5 :
:: deftheorem Def6 defines closed_interval MEASURE5:def 6 :
:: deftheorem Def7 defines right_open_interval MEASURE5:def 7 :
:: deftheorem Def8 defines left_open_interval MEASURE5:def 8 :
:: deftheorem Def9 defines interval MEASURE5:def 9 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th17:
theorem
theorem
:: deftheorem Def10 defines diameter MEASURE5:def 10 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
Lm1:
for A being Interval holds diameter A >= 0
Lm2:
for A, B being Interval st A c= B holds
diameter A <= diameter B
theorem
theorem
theorem