:: Properties of the Intervals of Real Numbers
:: by J\'ozef Bia{\l}as
::
:: Received January 12, 1993
:: Copyright (c) 1993 Association of Mizar Users
theorem :: MEASURE5:1
canceled;
theorem :: MEASURE5:2
canceled;
theorem :: MEASURE5:3
canceled;
theorem :: MEASURE5:4
canceled;
theorem :: MEASURE5:5
canceled;
theorem :: MEASURE5:6
canceled;
theorem :: MEASURE5:7
canceled;
theorem :: MEASURE5:8
:: 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 :: MEASURE5:9
canceled;
theorem :: MEASURE5:10
canceled;
theorem :: MEASURE5:11
canceled;
theorem :: MEASURE5:12
canceled;
theorem :: MEASURE5:13
canceled;
theorem :: MEASURE5:14
canceled;
theorem :: MEASURE5:15
canceled;
theorem :: MEASURE5:16
canceled;
theorem Th17: :: MEASURE5:17
theorem :: MEASURE5:18
theorem :: MEASURE5:19
:: deftheorem Def10 defines diameter MEASURE5:def 10 :
theorem :: MEASURE5:20
canceled;
theorem :: MEASURE5:21
canceled;
theorem :: MEASURE5:22
canceled;
theorem :: MEASURE5:23
canceled;
theorem :: MEASURE5:24
canceled;
theorem :: MEASURE5:25
canceled;
theorem :: MEASURE5:26
canceled;
theorem :: MEASURE5:27
canceled;
theorem :: MEASURE5:28
canceled;
theorem :: MEASURE5:29
canceled;
theorem :: MEASURE5:30
canceled;
theorem :: MEASURE5:31
canceled;
theorem :: MEASURE5:32
canceled;
theorem :: MEASURE5:33
canceled;
theorem :: MEASURE5:34
canceled;
theorem :: MEASURE5:35
canceled;
theorem :: MEASURE5:36
canceled;
theorem :: MEASURE5:37
canceled;
theorem :: MEASURE5:38
canceled;
theorem :: MEASURE5:39
canceled;
theorem :: MEASURE5:40
canceled;
theorem :: MEASURE5:41
canceled;
theorem :: MEASURE5:42
canceled;
theorem :: MEASURE5:43
canceled;
theorem :: MEASURE5:44
canceled;
theorem :: MEASURE5:45
canceled;
theorem :: MEASURE5:46
canceled;
theorem :: MEASURE5:47
canceled;
theorem :: MEASURE5:48
canceled;
theorem :: MEASURE5:49
canceled;
theorem :: MEASURE5:50
canceled;
theorem :: MEASURE5:51
canceled;
theorem :: MEASURE5:52
canceled;
theorem :: MEASURE5:53
canceled;
theorem :: MEASURE5:54
theorem :: MEASURE5:55
theorem :: MEASURE5:56
theorem :: MEASURE5:57
theorem :: MEASURE5:58
canceled;
theorem :: MEASURE5:59
theorem Th60: :: MEASURE5:60
LX3:
for A being Interval holds diameter A >= 0
LX4:
for A, B being Interval st A c= B holds
diameter A <= diameter B
theorem :: MEASURE5:61
theorem :: MEASURE5:62
theorem :: MEASURE5:63