:: XREAL_0 semantic presentation

begin

definition
let r be ( ( ) ( ) number ) ;
attr r is real means :: XREAL_0:def 1
r : ( ( ext-real ) ( ext-real ) set ) in REAL : ( ( ) ( non empty ) set ) ;
end;

registration
cluster -> real for ( ( ) ( ) Element of REAL : ( ( ) ( non empty ) set ) ) ;
end;

registration
cluster -infty : ( ( ) ( non empty ext-real non positive negative ) set ) -> non real ;
cluster +infty : ( ( ) ( non empty ext-real positive non negative ) set ) -> non real ;
end;

registration
cluster natural -> real for ( ( ) ( ) set ) ;
cluster real -> complex for ( ( ) ( ) set ) ;
end;

registration
cluster real for ( ( ) ( ) set ) ;
cluster real -> ext-real for ( ( ) ( ) set ) ;
end;

registration
let x be ( ( real ) ( complex ext-real real ) number ) ;
cluster - x : ( ( real ) ( complex ext-real real ) set ) : ( ( complex ) ( complex ) set ) -> complex real ;
cluster x : ( ( real ) ( complex ext-real real ) set ) " : ( ( complex ) ( complex ) set ) -> complex real ;
let y be ( ( real ) ( complex ext-real real ) number ) ;
cluster x : ( ( real ) ( complex ext-real real ) set ) + y : ( ( real ) ( complex ext-real real ) set ) : ( ( ) ( complex ) set ) -> real ;
cluster x : ( ( real ) ( complex ext-real real ) set ) * y : ( ( real ) ( complex ext-real real ) set ) : ( ( ) ( complex ) set ) -> real ;
end;

registration
let x, y be ( ( real ) ( complex ext-real real ) number ) ;
cluster x : ( ( real ) ( complex ext-real real ) set ) - y : ( ( real ) ( complex ext-real real ) set ) : ( ( ) ( complex ) set ) -> real ;
cluster x : ( ( real ) ( complex ext-real real ) set ) / y : ( ( real ) ( complex ext-real real ) set ) : ( ( ) ( complex ) set ) -> real ;
end;

begin

registration
cluster complex ext-real positive real for ( ( ) ( ) set ) ;
cluster complex ext-real negative real for ( ( ) ( ) set ) ;
cluster zero complex ext-real real for ( ( ) ( ) set ) ;
end;

registration
let r, s be ( ( non negative real ) ( complex ext-real non negative real ) number ) ;
cluster r : ( ( non negative real ) ( complex ext-real non negative real ) set ) + s : ( ( non negative real ) ( complex ext-real non negative real ) set ) : ( ( ) ( complex ext-real real ) set ) -> non negative ;
end;

registration
let r, s be ( ( non positive real ) ( complex ext-real non positive real ) number ) ;
cluster r : ( ( non positive real ) ( complex ext-real non positive real ) set ) + s : ( ( non positive real ) ( complex ext-real non positive real ) set ) : ( ( ) ( complex ext-real real ) set ) -> non positive ;
end;

registration
let r be ( ( positive real ) ( non empty complex ext-real positive non negative real ) number ) ;
let s be ( ( non negative real ) ( complex ext-real non negative real ) number ) ;
cluster r : ( ( positive real ) ( non empty complex ext-real positive non negative real ) set ) + s : ( ( non negative real ) ( complex ext-real non negative real ) set ) : ( ( ) ( complex ext-real non negative real ) set ) -> positive ;
cluster s : ( ( non negative real ) ( complex ext-real non negative real ) set ) + r : ( ( positive real ) ( non empty complex ext-real positive non negative real ) set ) : ( ( ) ( complex ext-real non negative real ) set ) -> positive ;
end;

registration
let r be ( ( negative real ) ( non empty complex ext-real non positive negative real ) number ) ;
let s be ( ( non positive real ) ( complex ext-real non positive real ) number ) ;
cluster r : ( ( negative real ) ( non empty complex ext-real non positive negative real ) set ) + s : ( ( non positive real ) ( complex ext-real non positive real ) set ) : ( ( ) ( complex ext-real non positive real ) set ) -> negative ;
cluster s : ( ( non positive real ) ( complex ext-real non positive real ) set ) + r : ( ( negative real ) ( non empty complex ext-real non positive negative real ) set ) : ( ( ) ( complex ext-real non positive real ) set ) -> negative ;
end;

registration
let r be ( ( non positive real ) ( complex ext-real non positive real ) number ) ;
cluster - r : ( ( non positive real ) ( complex ext-real non positive real ) set ) : ( ( complex ) ( complex ext-real real ) set ) -> complex non negative ;
end;

registration
let r be ( ( non negative real ) ( complex ext-real non negative real ) number ) ;
cluster - r : ( ( non negative real ) ( complex ext-real non negative real ) set ) : ( ( complex ) ( complex ext-real real ) set ) -> complex non positive ;
end;

registration
let r be ( ( non negative real ) ( complex ext-real non negative real ) number ) ;
let s be ( ( non positive real ) ( complex ext-real non positive real ) number ) ;
cluster r : ( ( non negative real ) ( complex ext-real non negative real ) set ) - s : ( ( non positive real ) ( complex ext-real non positive real ) set ) : ( ( ) ( complex ext-real real ) set ) -> non negative ;
cluster s : ( ( non positive real ) ( complex ext-real non positive real ) set ) - r : ( ( non negative real ) ( complex ext-real non negative real ) set ) : ( ( ) ( complex ext-real real ) set ) -> non positive ;
end;

registration
let r be ( ( positive real ) ( non empty complex ext-real positive non negative real ) number ) ;
let s be ( ( non positive real ) ( complex ext-real non positive real ) number ) ;
cluster r : ( ( positive real ) ( non empty complex ext-real positive non negative real ) set ) - s : ( ( non positive real ) ( complex ext-real non positive real ) set ) : ( ( ) ( complex ext-real non negative real ) set ) -> positive ;
cluster s : ( ( non positive real ) ( complex ext-real non positive real ) set ) - r : ( ( positive real ) ( non empty complex ext-real positive non negative real ) set ) : ( ( ) ( complex ext-real non positive real ) set ) -> negative ;
end;

registration
let r be ( ( negative real ) ( non empty complex ext-real non positive negative real ) number ) ;
let s be ( ( non negative real ) ( complex ext-real non negative real ) number ) ;
cluster r : ( ( negative real ) ( non empty complex ext-real non positive negative real ) set ) - s : ( ( non negative real ) ( complex ext-real non negative real ) set ) : ( ( ) ( complex ext-real non positive real ) set ) -> negative ;
cluster s : ( ( non negative real ) ( complex ext-real non negative real ) set ) - r : ( ( negative real ) ( non empty complex ext-real non positive negative real ) set ) : ( ( ) ( complex ext-real non negative real ) set ) -> positive ;
end;

registration
let r be ( ( non positive real ) ( complex ext-real non positive real ) number ) ;
let s be ( ( non negative real ) ( complex ext-real non negative real ) number ) ;
cluster r : ( ( non positive real ) ( complex ext-real non positive real ) set ) * s : ( ( non negative real ) ( complex ext-real non negative real ) set ) : ( ( ) ( complex ext-real real ) set ) -> non positive ;
cluster s : ( ( non negative real ) ( complex ext-real non negative real ) set ) * r : ( ( non positive real ) ( complex ext-real non positive real ) set ) : ( ( ) ( complex ext-real real ) set ) -> non positive ;
end;

registration
let r, s be ( ( non positive real ) ( complex ext-real non positive real ) number ) ;
cluster r : ( ( non positive real ) ( complex ext-real non positive real ) set ) * s : ( ( non positive real ) ( complex ext-real non positive real ) set ) : ( ( ) ( complex ext-real real ) set ) -> non negative ;
end;

registration
let r, s be ( ( non negative real ) ( complex ext-real non negative real ) number ) ;
cluster r : ( ( non negative real ) ( complex ext-real non negative real ) set ) * s : ( ( non negative real ) ( complex ext-real non negative real ) set ) : ( ( ) ( complex ext-real real ) set ) -> non negative ;
end;

registration
let r be ( ( positive real ) ( non empty complex ext-real positive non negative real ) number ) ;
cluster r : ( ( positive real ) ( non empty complex ext-real positive non negative real ) set ) " : ( ( complex ) ( non empty complex ext-real real ) set ) -> complex positive ;
end;

registration
let r be ( ( non positive real ) ( complex ext-real non positive real ) number ) ;
cluster r : ( ( non positive real ) ( complex ext-real non positive real ) set ) " : ( ( complex ) ( complex ext-real real ) set ) -> complex non positive ;
end;

registration
let r be ( ( negative real ) ( non empty complex ext-real non positive negative real ) number ) ;
cluster r : ( ( negative real ) ( non empty complex ext-real non positive negative real ) set ) " : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) -> complex negative ;
end;

registration
let r be ( ( non negative real ) ( complex ext-real non negative real ) number ) ;
cluster r : ( ( non negative real ) ( complex ext-real non negative real ) set ) " : ( ( complex ) ( complex ext-real real ) set ) -> complex non negative ;
end;

registration
let r be ( ( non negative real ) ( complex ext-real non negative real ) number ) ;
let s be ( ( non positive real ) ( complex ext-real non positive real ) number ) ;
cluster r : ( ( non negative real ) ( complex ext-real non negative real ) set ) / s : ( ( non positive real ) ( complex ext-real non positive real ) set ) : ( ( ) ( complex ext-real real ) set ) -> non positive ;
cluster s : ( ( non positive real ) ( complex ext-real non positive real ) set ) / r : ( ( non negative real ) ( complex ext-real non negative real ) set ) : ( ( ) ( complex ext-real real ) set ) -> non positive ;
end;

registration
let r, s be ( ( non negative real ) ( complex ext-real non negative real ) number ) ;
cluster r : ( ( non negative real ) ( complex ext-real non negative real ) set ) / s : ( ( non negative real ) ( complex ext-real non negative real ) set ) : ( ( ) ( complex ext-real real ) set ) -> non negative ;
end;

registration
let r, s be ( ( non positive real ) ( complex ext-real non positive real ) number ) ;
cluster r : ( ( non positive real ) ( complex ext-real non positive real ) set ) / s : ( ( non positive real ) ( complex ext-real non positive real ) set ) : ( ( ) ( complex ext-real real ) set ) -> non negative ;
end;

begin

registration
let r, s be ( ( real ) ( complex ext-real real ) number ) ;
cluster min (r : ( ( real ) ( complex ext-real real ) set ) ,s : ( ( real ) ( complex ext-real real ) set ) ) : ( ( ) ( ext-real ) set ) -> real ;
cluster max (r : ( ( real ) ( complex ext-real real ) set ) ,s : ( ( real ) ( complex ext-real real ) set ) ) : ( ( ) ( ext-real ) set ) -> real ;
end;

definition
let r, s be ( ( real ) ( complex ext-real real ) number ) ;
func r -' s -> ( ( ) ( ) set ) equals :: XREAL_0:def 2
r : ( ( ) ( ) set ) - s : ( ( real ) ( complex ext-real real ) set ) : ( ( ) ( ) set ) if r : ( ( ) ( ) set ) - s : ( ( real ) ( complex ext-real real ) set ) : ( ( ) ( ) set ) >= 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) )
otherwise 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;
end;

registration
let r, s be ( ( real ) ( complex ext-real real ) number ) ;
cluster r : ( ( real ) ( complex ext-real real ) set ) -' s : ( ( real ) ( complex ext-real real ) set ) : ( ( ) ( ) set ) -> real ;
end;

registration
let r, s be ( ( real ) ( complex ext-real real ) number ) ;
cluster r : ( ( real ) ( complex ext-real real ) set ) -' s : ( ( real ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) set ) -> non negative real for ( ( real ) ( complex ext-real real ) number ) ;
end;