:: On the Sets Inhabited by Numbers
:: by Andrzej Trybulec
::
:: Received August 23, 2003
:: Copyright (c) 2003 Association of Mizar Users
:: deftheorem Def1 defines complex-membered MEMBERED:def 1 :
:: deftheorem Def2 defines ext-real-membered MEMBERED:def 2 :
:: deftheorem Def3 defines real-membered MEMBERED:def 3 :
:: deftheorem Def4 defines rational-membered MEMBERED:def 4 :
:: deftheorem Def5 defines integer-membered MEMBERED:def 5 :
:: deftheorem Def6 defines natural-membered MEMBERED:def 6 :
theorem Th1: :: MEMBERED:1
theorem Th2: :: MEMBERED:2
theorem Th3: :: MEMBERED:3
theorem Th4: :: MEMBERED:4
theorem Th5: :: MEMBERED:5
theorem Th6: :: MEMBERED:6
theorem :: MEMBERED:7
theorem :: MEMBERED:8
theorem :: MEMBERED:9
theorem :: MEMBERED:10
theorem :: MEMBERED:11
theorem :: MEMBERED:12
theorem :: MEMBERED:13
theorem :: MEMBERED:14
theorem :: MEMBERED:15
theorem :: MEMBERED:16
theorem :: MEMBERED:17
theorem :: MEMBERED:18
theorem Th19: :: MEMBERED:19
theorem Th20: :: MEMBERED:20
theorem Th21: :: MEMBERED:21
theorem Th22: :: MEMBERED:22
theorem Th23: :: MEMBERED:23
theorem Th24: :: MEMBERED:24
:: deftheorem Def7 defines c= MEMBERED:def 7 :
:: deftheorem Def8 defines c= MEMBERED:def 8 :
:: deftheorem Def9 defines c= MEMBERED:def 9 :
:: deftheorem Def10 defines c= MEMBERED:def 10 :
:: deftheorem Def11 defines c= MEMBERED:def 11 :
:: deftheorem Def12 defines c= MEMBERED:def 12 :
:: deftheorem defines = MEMBERED:def 13 :
:: deftheorem defines = MEMBERED:def 14 :
:: deftheorem defines = MEMBERED:def 15 :
:: deftheorem defines = MEMBERED:def 16 :
:: deftheorem defines = MEMBERED:def 17 :
:: deftheorem defines = MEMBERED:def 18 :
:: deftheorem defines meets MEMBERED:def 19 :
:: deftheorem defines meets MEMBERED:def 20 :
:: deftheorem defines meets MEMBERED:def 21 :
:: deftheorem defines meets MEMBERED:def 22 :
:: deftheorem defines meets MEMBERED:def 23 :
:: deftheorem defines meets MEMBERED:def 24 :
theorem :: MEMBERED:25
theorem :: MEMBERED:26
theorem :: MEMBERED:27
theorem :: MEMBERED:28
theorem :: MEMBERED:29
theorem :: MEMBERED:30
theorem :: MEMBERED:31
theorem :: MEMBERED:32
theorem :: MEMBERED:33
theorem :: MEMBERED:34
theorem :: MEMBERED:35
theorem :: MEMBERED:36
theorem :: MEMBERED:37