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 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 :
for
a,
b being
R_eal for
b3 being
Subset of holds
(
b3 = ].a,b.[ iff for
x being
R_eal holds
(
x in b3 iff (
a < x &
x < b ) ) );
:: 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