The abstract of the Mizar article:

Subsets of Complex Numbers

by

Andrzej Trybulec

Received November 7, 2003

MML identifier: NUMBERS

[ Mizar article, MML identifier index ]

environ

 vocabulary COMPLEX1, FUNCT_2, FUNCT_1, FUNCOP_1, ARYTM_2, BOOLE, ARYTM_3,
      ORDINAL2, ARYTM, ORDINAL1, RELAT_1, RAT_1, INT_1, ORDINAL3;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
      FUNCT_4, ORDINAL1, ORDINAL2, ORDINAL3, ARYTM_3, ARYTM_2;
 constructors ARYTM_1, FRAENKEL, FUNCT_4, ORDINAL3;
 clusters XBOOLE_0, ARYTM_2, SUBSET_1, ORDINAL2, ARYTM_3, FRAENKEL, FUNCT_2,
      FUNCT_4, ORDINAL1, ZFMISC_1;
 requirements BOOLE, SUBSET, NUMERALS;


begin

definition
 func REAL equals
:: NUMBERS:def 1
 REAL+ \/ [:{0},REAL+:] \ {[0,0]};
 redefine func omega; synonym NAT;
end;

definition
 cluster REAL -> non empty;
end;

definition
 func COMPLEX equals
:: NUMBERS:def 2
 Funcs({0,one},REAL)
        \ { x where x is Element of Funcs({0,one},REAL): x.one = 0}
        \/ REAL;
 func RAT equals
:: NUMBERS:def 3
 RAT+ \/ [:{0},RAT+:] \ {[0,0]};
 func INT equals
:: NUMBERS:def 4
 NAT \/ [:{0},NAT:] \ {[0,0]};
 redefine func NAT -> Subset of REAL;
end;

definition
 cluster COMPLEX -> non empty;
 cluster RAT -> non empty;
 cluster INT -> non empty;
end;

reserve i,j,k for Element of NAT;
reserve a,b for Element of REAL;

theorem :: NUMBERS:1
 REAL c< COMPLEX;

reserve r,s,t for Element of RAT+;
reserve i,j,k for Element of omega;

theorem :: NUMBERS:2
 RAT c< REAL;

theorem :: NUMBERS:3
 RAT c< COMPLEX;

theorem :: NUMBERS:4
 INT c< RAT;

theorem :: NUMBERS:5
 INT c< REAL;

theorem :: NUMBERS:6
 INT c< COMPLEX;

theorem :: NUMBERS:7
 NAT c< INT;

theorem :: NUMBERS:8
 NAT c< RAT;

theorem :: NUMBERS:9
 NAT c< REAL;

theorem :: NUMBERS:10
 NAT c< COMPLEX;

begin :: to be canceled

theorem :: NUMBERS:11
 REAL c= COMPLEX;

theorem :: NUMBERS:12
 RAT c= REAL;

theorem :: NUMBERS:13
 RAT c= COMPLEX;

theorem :: NUMBERS:14
 INT c= RAT;

theorem :: NUMBERS:15
 INT c= REAL;

theorem :: NUMBERS:16
 INT c= COMPLEX;

theorem :: NUMBERS:17
 NAT c= INT;

theorem :: NUMBERS:18
 NAT c= RAT;

theorem :: NUMBERS:19
 NAT c= REAL;

theorem :: NUMBERS:20
 NAT c= COMPLEX;

theorem :: NUMBERS:21
 REAL <> COMPLEX;

theorem :: NUMBERS:22
 RAT <> REAL;

theorem :: NUMBERS:23
 RAT <> COMPLEX;

theorem :: NUMBERS:24
 INT <> RAT;

theorem :: NUMBERS:25
 INT <> REAL;

theorem :: NUMBERS:26
 INT <> COMPLEX;

theorem :: NUMBERS:27
 NAT <> INT;

theorem :: NUMBERS:28
 NAT <> RAT;

theorem :: NUMBERS:29
 NAT <> REAL;

theorem :: NUMBERS:30
 NAT <> COMPLEX;