:: NUMBERS semantic presentation

begin

notation
synonym NAT for omega ;
synonym 0 for {} ;
end;

definition
func REAL -> ( ( ) ( ) set ) equals :: NUMBERS:def 1
(REAL+ : ( ( ) ( non empty ) set ) \/ [:{0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) } : ( ( ) ( non empty ) set ) ,REAL+ : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) \ {[0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ] : ( ( ) ( V15() ) set ) } : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( ) Element of bool (REAL+ : ( ( ) ( non empty ) set ) \/ [:{0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) } : ( ( ) ( non empty ) set ) ,REAL+ : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
cluster REAL : ( ( ) ( ) set ) -> non empty ;
end;

definition
func COMPLEX -> ( ( ) ( ) set ) equals :: NUMBERS:def 2
((Funcs ({0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty ) set ) )) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of {0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty ) set ) ) \ { x : ( ( ) ( Relation-like Function-like V14({0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) ) quasi_total ) Element of Funcs ({0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of {0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty ) set ) ) ) where x is ( ( ) ( Relation-like Function-like V14({0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) ) quasi_total ) Element of Funcs ({0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of {0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty ) set ) ) ) : x : ( ( ) ( Relation-like Function-like V14({0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) ) quasi_total ) Element of Funcs ({0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of {0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty ) set ) ) ) . 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) : ( ( ) ( ) set ) = 0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) } ) : ( ( ) ( ) Element of bool (Funcs ({0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty ) set ) )) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of {0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) \/ REAL : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ;
func RAT -> ( ( ) ( ) set ) equals :: NUMBERS:def 3
(RAT+ : ( ( ) ( non empty ) set ) \/ [:{0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) } : ( ( ) ( non empty ) set ) ,RAT+ : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) \ {[0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ] : ( ( ) ( V15() ) set ) } : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( ) Element of bool (RAT+ : ( ( ) ( non empty ) set ) \/ [:{0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) } : ( ( ) ( non empty ) set ) ,RAT+ : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;
func INT -> ( ( ) ( ) set ) equals :: NUMBERS:def 4
(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) \/ [:{0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) } : ( ( ) ( non empty ) set ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) :] : ( ( ) ( Relation-like non finite ) set ) ) : ( ( ) ( non empty ) set ) \ {[0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ] : ( ( ) ( V15() ) set ) } : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( ) Element of bool (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) \/ [:{0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) } : ( ( ) ( non empty ) set ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) :] : ( ( ) ( Relation-like non finite ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;
:: original: NAT
redefine func NAT -> ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ;
end;

registration
cluster COMPLEX : ( ( ) ( ) set ) -> non empty ;
cluster RAT : ( ( ) ( ) set ) -> non empty ;
cluster INT : ( ( ) ( ) set ) -> non empty ;
end;

definition
:: original: 0
redefine func 0 -> ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) Subset of ( ( ) ( ) set ) ) ) ;
end;

theorem :: NUMBERS:1
REAL : ( ( ) ( non empty ) set ) c< COMPLEX : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:2
RAT : ( ( ) ( non empty ) set ) c< REAL : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:3
RAT : ( ( ) ( non empty ) set ) c< COMPLEX : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:4
INT : ( ( ) ( non empty ) set ) c< RAT : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:5
INT : ( ( ) ( non empty ) set ) c< REAL : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:6
INT : ( ( ) ( non empty ) set ) c< COMPLEX : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:7
NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) Subset of ( ( ) ( ) set ) ) c< INT : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:8
NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) Subset of ( ( ) ( ) set ) ) c< RAT : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:9
NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) Subset of ( ( ) ( ) set ) ) c< REAL : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:10
NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) Subset of ( ( ) ( ) set ) ) c< COMPLEX : ( ( ) ( non empty ) set ) ;

begin

theorem :: NUMBERS:11
REAL : ( ( ) ( non empty ) set ) c= COMPLEX : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:12
RAT : ( ( ) ( non empty ) set ) c= REAL : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:13
RAT : ( ( ) ( non empty ) set ) c= COMPLEX : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:14
INT : ( ( ) ( non empty ) set ) c= RAT : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:15
INT : ( ( ) ( non empty ) set ) c= REAL : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:16
INT : ( ( ) ( non empty ) set ) c= COMPLEX : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:17
NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) Subset of ( ( ) ( ) set ) ) c= INT : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:18
NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) Subset of ( ( ) ( ) set ) ) c= RAT : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:19
NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) Subset of ( ( ) ( ) set ) ) c= REAL : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:20
NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) Subset of ( ( ) ( ) set ) ) c= COMPLEX : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:21
REAL : ( ( ) ( non empty ) set ) <> COMPLEX : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:22
RAT : ( ( ) ( non empty ) set ) <> REAL : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:23
RAT : ( ( ) ( non empty ) set ) <> COMPLEX : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:24
INT : ( ( ) ( non empty ) set ) <> RAT : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:25
INT : ( ( ) ( non empty ) set ) <> REAL : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:26
INT : ( ( ) ( non empty ) set ) <> COMPLEX : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:27
NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) Subset of ( ( ) ( ) set ) ) <> INT : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:28
NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) Subset of ( ( ) ( ) set ) ) <> RAT : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:29
NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) Subset of ( ( ) ( ) set ) ) <> REAL : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:30
NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) Subset of ( ( ) ( ) set ) ) <> COMPLEX : ( ( ) ( non empty ) set ) ;

definition
func ExtREAL -> ( ( ) ( ) set ) equals :: NUMBERS:def 5
REAL : ( ( ) ( non empty ) set ) \/ {REAL : ( ( ) ( non empty ) set ) ,[0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) Subset of ( ( ) ( ) set ) ) ) ,REAL : ( ( ) ( non empty ) set ) ] : ( ( ) ( V15() ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ;
end;

registration
cluster ExtREAL : ( ( ) ( ) set ) -> non empty ;
end;

theorem :: NUMBERS:31
REAL : ( ( ) ( non empty ) set ) c= ExtREAL : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:32
REAL : ( ( ) ( non empty ) set ) <> ExtREAL : ( ( ) ( non empty ) set ) ;

theorem :: NUMBERS:33
REAL : ( ( ) ( non empty ) set ) c< ExtREAL : ( ( ) ( non empty ) set ) ;

registration
cluster INT : ( ( ) ( non empty ) set ) -> infinite ;
cluster RAT : ( ( ) ( non empty ) set ) -> infinite ;
cluster REAL : ( ( ) ( non empty ) set ) -> infinite ;
cluster COMPLEX : ( ( ) ( non empty ) set ) -> infinite ;
end;