:: Real Function Uniform Continuity
:: by Jaros{\l}aw Kotowicz and Konrad Raczkowski
::
:: Received June 18, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Xdef defines uniformly_continuous FCONT_2:def 1 :
theorem Def1: :: FCONT_2:1
theorem Th2: :: FCONT_2:2
theorem :: FCONT_2:3
theorem :: FCONT_2:4
theorem Th5: :: FCONT_2:5
theorem :: FCONT_2:6
theorem :: FCONT_2:7
theorem :: FCONT_2:8
theorem Th9: :: FCONT_2:9
theorem Th10: :: FCONT_2:10
theorem Th11: :: FCONT_2:11
theorem :: FCONT_2:12
canceled;
theorem :: FCONT_2:13
theorem :: FCONT_2:14
theorem :: FCONT_2:15
theorem Th16: :: FCONT_2:16
theorem Th17: :: FCONT_2:17
theorem Th18: :: FCONT_2:18
theorem :: FCONT_2:19
theorem Th20: :: FCONT_2:20
theorem :: FCONT_2:21