:: The "Way-Below" Relation
:: by Grzegorz Bancerek
::
:: Received October 11, 1996
:: Copyright (c) 1996 Association of Mizar Users
:: deftheorem Def1 defines is_way_below WAYBEL_3:def 1 :
:: deftheorem Def2 defines compact WAYBEL_3:def 2 :
theorem Th1: :: WAYBEL_3:1
theorem Th2: :: WAYBEL_3:2
theorem Th3: :: WAYBEL_3:3
theorem Th4: :: WAYBEL_3:4
theorem :: WAYBEL_3:5
theorem :: WAYBEL_3:6
:: deftheorem defines waybelow WAYBEL_3:def 3 :
:: deftheorem defines wayabove WAYBEL_3:def 4 :
theorem Th7: :: WAYBEL_3:7
theorem Th8: :: WAYBEL_3:8
theorem Th9: :: WAYBEL_3:9
theorem :: WAYBEL_3:10
theorem Th11: :: WAYBEL_3:11
theorem Th12: :: WAYBEL_3:12
theorem Th13: :: WAYBEL_3:13
theorem :: WAYBEL_3:14
theorem :: WAYBEL_3:15
theorem Th16: :: WAYBEL_3:16
theorem :: WAYBEL_3:17
theorem Th18: :: WAYBEL_3:18
theorem :: WAYBEL_3:19
theorem :: WAYBEL_3:20
theorem Th21: :: WAYBEL_3:21
theorem :: WAYBEL_3:22
theorem :: WAYBEL_3:23
:: deftheorem Def5 defines satisfying_axiom_of_approximation WAYBEL_3:def 5 :
:: deftheorem Def6 defines continuous WAYBEL_3:def 6 :
theorem :: WAYBEL_3:24
theorem :: WAYBEL_3:25
theorem :: WAYBEL_3:26
:: deftheorem Def7 defines non-Empty WAYBEL_3:def 7 :
:: deftheorem Def8 defines reflexive-yielding WAYBEL_3:def 8 :
theorem Th27: :: WAYBEL_3:27
theorem Th28: :: WAYBEL_3:28
theorem Th29: :: WAYBEL_3:29
theorem Th30: :: WAYBEL_3:30
theorem Th31: :: WAYBEL_3:31
theorem Th32: :: WAYBEL_3:32
theorem :: WAYBEL_3:33
theorem Th34: :: WAYBEL_3:34
theorem Th35: :: WAYBEL_3:35
theorem Th36: :: WAYBEL_3:36
theorem :: WAYBEL_3:37
:: deftheorem Def9 defines locally-compact WAYBEL_3:def 9 :
theorem :: WAYBEL_3:38
canceled;
theorem Th39: :: WAYBEL_3:39
theorem Th40: :: WAYBEL_3:40
theorem :: WAYBEL_3:41
theorem :: WAYBEL_3:42
theorem :: WAYBEL_3:43