:: XREAL_1 semantic presentation

begin

theorem :: XREAL_1:1
for a being ( ( real ) ( complex ext-real real ) number ) ex b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:2
for a being ( ( real ) ( complex ext-real real ) number ) ex b being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < a : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:3
for a, b being ( ( real ) ( complex ext-real real ) number ) ex c being ( ( real ) ( complex ext-real real ) number ) st
( a : ( ( real ) ( complex ext-real real ) number ) < c : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) < c : ( ( real ) ( complex ext-real real ) number ) ) ;

theorem :: XREAL_1:4
for a, b being ( ( real ) ( complex ext-real real ) number ) ex c being ( ( real ) ( complex ext-real real ) number ) st
( c : ( ( real ) ( complex ext-real real ) number ) < a : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) ) ;

theorem :: XREAL_1:5
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) holds
ex c being ( ( real ) ( complex ext-real real ) number ) st
( a : ( ( real ) ( complex ext-real real ) number ) < c : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) ) ;

begin

theorem :: XREAL_1:6
for a, b, c being ( ( real ) ( complex ext-real real ) number ) holds
( a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) iff a : ( ( real ) ( complex ext-real real ) number ) + c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) + c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ) ;

theorem :: XREAL_1:7
for a, b, c, d being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) <= d : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) + c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) + d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:8
for a, b, c, d being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) <= d : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) + c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) + d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

begin

theorem :: XREAL_1:9
for a, b, c being ( ( real ) ( complex ext-real real ) number ) holds
( a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) iff a : ( ( real ) ( complex ext-real real ) number ) - c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) - c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ) ;

theorem :: XREAL_1:10
for a, b, c being ( ( real ) ( complex ext-real real ) number ) holds
( a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) iff c : ( ( real ) ( complex ext-real real ) number ) - b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ) ;

theorem :: XREAL_1:11
for a, b, c being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) - c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
c : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:12
for a, b, c being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) - b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) - c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:13
for a, b, c, d being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) <= d : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) - d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) - c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:14
for a, b, c, d being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) <= d : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) - d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) - c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:15
for a, b, c, d being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) < d : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) - d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) - c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:16
for a, b, c, d being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) - b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) - d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) - c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) - d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:17
for a, b, c, d being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) - b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) - d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
d : ( ( real ) ( complex ext-real real ) number ) - b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:18
for a, b, c, d being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) - b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) - d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
d : ( ( real ) ( complex ext-real real ) number ) - c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

begin

theorem :: XREAL_1:19
for a, b, c being ( ( real ) ( complex ext-real real ) number ) holds
( a : ( ( real ) ( complex ext-real real ) number ) + b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) iff a : ( ( real ) ( complex ext-real real ) number ) <= c : ( ( real ) ( complex ext-real real ) number ) - b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ) ;

theorem :: XREAL_1:20
for a, b, c being ( ( real ) ( complex ext-real real ) number ) holds
( a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) + c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) iff a : ( ( real ) ( complex ext-real real ) number ) - b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) ) ;

theorem :: XREAL_1:21
for a, b, c, d being ( ( real ) ( complex ext-real real ) number ) holds
( a : ( ( real ) ( complex ext-real real ) number ) + b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) + d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) iff a : ( ( real ) ( complex ext-real real ) number ) - c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= d : ( ( real ) ( complex ext-real real ) number ) - b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ) ;

theorem :: XREAL_1:22
for a, b, c, d being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) + b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) - d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) + d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) - b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:23
for a, b, c, d being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) - b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) + d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) - d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) + b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

begin

theorem :: XREAL_1:24
for a, b being ( ( real ) ( complex ext-real real ) number ) holds
( a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) iff - b : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) <= - a : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) ) ;

theorem :: XREAL_1:25
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= - b : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) holds
b : ( ( real ) ( complex ext-real real ) number ) <= - a : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:26
for b, a being ( ( real ) ( complex ext-real real ) number ) st - b : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) holds
- a : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) ;

begin

theorem :: XREAL_1:27
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) <= b : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) + b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) 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 ) ) ) holds
a : ( ( real ) ( complex ext-real real ) number ) = 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 ) ) ) ;

theorem :: XREAL_1:28
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) + b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) 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 ) ) ) holds
a : ( ( real ) ( complex ext-real real ) number ) = 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 ) ) ) ;

begin

theorem :: XREAL_1:29
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) + a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:30
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) holds
a : ( ( real ) ( complex ext-real real ) number ) + b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:31
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) + b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:32
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) holds
a : ( ( real ) ( complex ext-real real ) number ) + b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) ;

begin

theorem :: XREAL_1:33
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) + b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:34
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) holds
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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) + b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:35
for a, c, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & c : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
c : ( ( real ) ( complex ext-real real ) number ) + a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:36
for a, c, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & c : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) holds
c : ( ( real ) ( complex ext-real real ) number ) + a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:37
for a, c, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & c : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
c : ( ( real ) ( complex ext-real real ) number ) + a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:38
for a, b, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) <= c : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) + c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:39
for a, b, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) <= c : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) < a : ( ( real ) ( complex ext-real real ) number ) + c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:40
for a, b, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) < c : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) < a : ( ( real ) ( complex ext-real real ) number ) + c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

begin

theorem :: XREAL_1:41
for c, b being ( ( real ) ( complex ext-real real ) number ) st ( for a being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) > 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 ) ) ) holds
c : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) + a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ) holds
c : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:42
for b, c being ( ( real ) ( complex ext-real real ) number ) st ( for a being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) holds
b : ( ( real ) ( complex ext-real real ) number ) + a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) ) holds
b : ( ( real ) ( complex ext-real real ) number ) <= c : ( ( real ) ( complex ext-real real ) number ) ;

begin

theorem :: XREAL_1:43
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:44
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:45
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) holds
b : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:46
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) holds
b : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:47
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) - b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) 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 ) ) ) ;

theorem :: XREAL_1:48
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
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 ) ) ) <= b : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:49
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) - b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) 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 ) ) ) ;

theorem :: XREAL_1:50
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) holds
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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:51
for a, b, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) < c : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:52
for a, b, c being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) <= c : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) <= c : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:53
for a, b, c being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) < c : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) < c : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:54
for a, b, c being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) <= c : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) < c : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:55
for a, b being ( ( real ) ( complex ext-real real ) number ) holds
( not a : ( ( real ) ( complex ext-real real ) number ) <> b : ( ( real ) ( complex ext-real real ) number ) or 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) - b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) or 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ) ;

begin

theorem :: XREAL_1:56
for c, b being ( ( real ) ( complex ext-real real ) number ) st ( for a being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) holds
c : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ) holds
b : ( ( real ) ( complex ext-real real ) number ) >= c : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:57
for b, c being ( ( real ) ( complex ext-real real ) number ) st ( for a being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) > 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 ) ) ) holds
b : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) ) holds
b : ( ( real ) ( complex ext-real real ) number ) <= c : ( ( real ) ( complex ext-real real ) number ) ;

begin

theorem :: XREAL_1:58
for a being ( ( real ) ( complex ext-real real ) number ) holds
( a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) iff 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 ) ) ) < - a : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) ) ;

theorem :: XREAL_1:59
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= - b : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) + b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) 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 ) ) ) ;

theorem :: XREAL_1:60
for a, b being ( ( real ) ( complex ext-real real ) number ) st - a : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) + b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:61
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < - b : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) + b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) 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 ) ) ) ;

theorem :: XREAL_1:62
for b, a being ( ( real ) ( complex ext-real real ) number ) st - b : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) holds
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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) + b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

begin

theorem :: XREAL_1:63
for a being ( ( real ) ( complex ext-real real ) number ) holds 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) * a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:64
for a, b, c being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) <= c : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:65
for a, b, c being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) holds
b : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:66
for a, b, c, d being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) <= c : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) <= d : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:67
for a, b, c, d being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & d : ( ( real ) ( complex ext-real real ) number ) <= c : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:68
for c, a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < c : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:69
for c, a, b being ( ( real ) ( complex ext-real real ) number ) st c : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:70
for a, b, c, d being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & d : ( ( real ) ( complex ext-real real ) number ) < c : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

begin

theorem :: XREAL_1:71
for a, b, c, d being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) <= b : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) <= c : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) <= d : ( ( real ) ( complex ext-real real ) number ) & (a : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) + (b : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) 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 ) ) ) & not a : ( ( real ) ( complex ext-real real ) number ) = 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 ) ) ) holds
c : ( ( real ) ( complex ext-real real ) number ) = 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 ) ) ) ;

begin

theorem :: XREAL_1:72
for c, b, a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= c : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) / c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) / c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:73
for c, a, b being ( ( real ) ( complex ext-real real ) number ) st c : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) / c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) / c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:74
for c, a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < c : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) / c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) / c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:75
for c, a, b being ( ( real ) ( complex ext-real real ) number ) st c : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) / c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) / c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:76
for c, a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < c : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) holds
c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

begin

theorem :: XREAL_1:77
for b, a, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) <= c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:78
for b, a, c being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) holds
c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:79
for b, c, a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:80
for b, c, a being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & c : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) <= c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:81
for b, a, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) < c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:82
for b, a, c being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) holds
c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:83
for b, c, a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) < a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:84
for b, c, a being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & c : ( ( real ) ( complex ext-real real ) number ) < a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) < c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

begin

theorem :: XREAL_1:85
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:86
for b, a being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:87
for b, a being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:88
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:89
for b, a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) & b : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:90
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:91
for b, a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) & b : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:92
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) ;

begin

theorem :: XREAL_1:93
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & (b : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) * (b : ( ( real ) ( complex ext-real real ) number ) + a : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) 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 ) ) ) holds
( - a : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) ) ;

theorem :: XREAL_1:94
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & (b : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) * (b : ( ( real ) ( complex ext-real real ) number ) + a : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) 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 ) ) ) holds
( - a : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) < a : ( ( real ) ( complex ext-real real ) number ) ) ;

theorem :: XREAL_1:95
for b, a being ( ( real ) ( complex ext-real real ) number ) holds
( not 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 ) ) ) <= (b : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) * (b : ( ( real ) ( complex ext-real real ) number ) + a : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) set ) or b : ( ( real ) ( complex ext-real real ) number ) <= - a : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) or a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) ) ;

theorem :: XREAL_1:96
for a, c, b, d being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) <= c : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) < d : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:97
for a, c, b, d being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) < c : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) <= d : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:98
for a, c, b, d being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) < c : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) < d : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:99
for c, b, a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < c : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) holds
c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:100
for c, a, b being ( ( real ) ( complex ext-real real ) number ) st c : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) holds
c : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:101
for c, b, a being ( ( real ) ( complex ext-real real ) number ) st c : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) holds
c : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:102
for b, d, a, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) < d : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) / d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:103
for b, d, a, c being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & d : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) / d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:104
for b, d, a, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & d : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
c : ( ( real ) ( complex ext-real real ) number ) / d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:105
for b, d, a, c being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & 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 ) ) ) < d : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
c : ( ( real ) ( complex ext-real real ) number ) / d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:106
for b, d, a, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) < d : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) / d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:107
for b, d, a, c being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & d : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) / d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:108
for b, d, a, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & d : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
c : ( ( real ) ( complex ext-real real ) number ) / d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:109
for b, d, a, c being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & 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 ) ) ) < d : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
c : ( ( real ) ( complex ext-real real ) number ) / d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:110
for b, d, a, c being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & d : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) / d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:111
for b, d, a, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) < d : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) / d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:112
for b, d, c, a being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & d : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & c : ( ( real ) ( complex ext-real real ) number ) / d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:113
for b, d, c, a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) < d : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) / d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:114
for b, d, a, c being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & 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 ) ) ) < d : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) / d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:115
for b, d, a, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & d : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) / d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:116
for b, d, c, a being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & 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 ) ) ) < d : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) / d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:117
for b, d, c, a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & d : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & c : ( ( real ) ( complex ext-real real ) number ) / d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) * d : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:118
for a, c, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) <= c : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:119
for c, b, a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= c : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:120
for c, a, b being ( ( real ) ( complex ext-real real ) number ) st c : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
c : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:121
for c, b, a being ( ( real ) ( complex ext-real real ) number ) st c : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
c : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:122
for a being ( ( real ) ( complex ext-real real ) number ) holds
( 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) iff 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) ) ;

theorem :: XREAL_1:123
for a being ( ( real ) ( complex ext-real real ) number ) holds
( a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) iff a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) 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 ) ) ) ) ;

theorem :: XREAL_1:124
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:125
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) 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 ) ) ) & 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) ;

begin

theorem :: XREAL_1:126
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) holds
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 ) ) ) = a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:127
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:128
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) holds
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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:129
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) holds
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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:130
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) holds
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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:131
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) holds
a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) 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 ) ) ) ;

theorem :: XREAL_1:132
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) holds
a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) 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 ) ) ) ;

theorem :: XREAL_1:133
for a, b being ( ( real ) ( complex ext-real real ) number ) holds
( not a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) 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 ) ) ) or ( a : ( ( real ) ( complex ext-real real ) number ) > 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) ) or ( a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) > 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 ) ) ) ) ) ;

theorem :: XREAL_1:134
for a, b being ( ( real ) ( complex ext-real real ) number ) holds
( not a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) 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 ) ) ) or ( a : ( ( real ) ( complex ext-real real ) number ) > 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) > 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 ) ) ) ) or ( a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) ) ) ;

theorem :: XREAL_1:135
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) holds
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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:136
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:137
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) 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 ) ) ) ;

theorem :: XREAL_1:138
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & 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 ) ) ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) 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 ) ) ) ;

theorem :: XREAL_1:139
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) holds
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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:140
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) holds
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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:141
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) 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 ) ) ) ;

theorem :: XREAL_1:142
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) 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 ) ) ) ;

theorem :: XREAL_1:143
for a, b being ( ( real ) ( complex ext-real real ) number ) holds
( not a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) 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 ) ) ) or ( b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) > 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 ) ) ) ) or ( b : ( ( real ) ( complex ext-real real ) number ) > 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) ) ) ;

theorem :: XREAL_1:144
for a, b being ( ( real ) ( complex ext-real real ) number ) holds
( not a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) 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 ) ) ) or ( b : ( ( real ) ( complex ext-real real ) number ) > 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) > 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 ) ) ) ) or ( b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) ) ) ;

begin

theorem :: XREAL_1:145
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:146
for a being ( ( real ) ( complex ext-real real ) number ) holds a : ( ( real ) ( complex ext-real real ) number ) - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:147
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:148
for a being ( ( real ) ( complex ext-real real ) number ) st - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) holds
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 ) ) ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) + a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:149
for a being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) holds
1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) 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 ) ) ) ;

begin

theorem :: XREAL_1:150
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) 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 ) ) ) <= b : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) = 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( complex ext-real real ) number ) = 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: XREAL_1:151
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:152
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:153
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:154
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:155
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) < a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:156
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( complex ext-real real ) number ) < a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:157
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:158
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:159
for a, b being ( ( real ) ( complex ext-real real ) number ) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:160
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: XREAL_1:161
for a, b being ( ( real ) ( complex ext-real real ) number ) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:162
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: XREAL_1:163
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) & b : ( ( real ) ( complex ext-real real ) number ) <= - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) holds
1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:164
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) & b : ( ( real ) ( complex ext-real real ) number ) <= - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) holds
1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:165
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) & - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: XREAL_1:166
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) & - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;

begin

theorem :: XREAL_1:167
for c, b being ( ( real ) ( complex ext-real real ) number ) st ( for a being ( ( real ) ( complex ext-real real ) number ) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) holds
c : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) * a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ) holds
c : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:168
for b, c being ( ( real ) ( complex ext-real real ) number ) st ( for a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) holds
b : ( ( real ) ( complex ext-real real ) number ) * a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) ) holds
b : ( ( real ) ( complex ext-real real ) number ) <= c : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:169
for b, c being ( ( real ) ( complex ext-real real ) number ) st ( for a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) holds
b : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ) holds
b : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) ;

theorem :: XREAL_1:170
for d, a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= d : ( ( real ) ( complex ext-real real ) number ) & d : ( ( real ) ( complex ext-real real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & 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 ) ) ) <= b : ( ( real ) ( complex ext-real real ) number ) & (d : ( ( real ) ( complex ext-real real ) number ) * a : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) + ((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) - d : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) * b : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) 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 ) ) ) & not ( d : ( ( real ) ( complex ext-real real ) number ) = 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) = 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 ) ) ) ) & not ( d : ( ( real ) ( complex ext-real real ) number ) = 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) = 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 ) ) ) ) holds
( a : ( ( real ) ( complex ext-real real ) number ) = 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) = 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 ) ) ) ) ;

theorem :: XREAL_1:171
for d, a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= d : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) <= ((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) - d : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) * a : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) + (d : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:172
for d, a, b being ( ( real ) ( complex ext-real real ) number ) st d : ( ( real ) ( complex ext-real real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) - d : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) * a : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) + (d : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:173
for d, a, b, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= d : ( ( real ) ( complex ext-real real ) number ) & d : ( ( real ) ( complex ext-real real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) <= c : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) <= ((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) - d : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) * b : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) + (d : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:174
for d, b, a, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= d : ( ( real ) ( complex ext-real real ) number ) & d : ( ( real ) ( complex ext-real real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) holds
((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) - d : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) * b : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) + (d : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:175
for d, a, b, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= d : ( ( real ) ( complex ext-real real ) number ) & d : ( ( real ) ( complex ext-real real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) < c : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) < ((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) - d : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) * b : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) + (d : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:176
for d, b, a, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= d : ( ( real ) ( complex ext-real real ) number ) & d : ( ( real ) ( complex ext-real real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) < a : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) < a : ( ( real ) ( complex ext-real real ) number ) holds
((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) - d : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) * b : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) + (d : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:177
for d, a, b, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < d : ( ( real ) ( complex ext-real real ) number ) & d : ( ( real ) ( complex ext-real real ) number ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) < c : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) < ((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) - d : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) * b : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) + (d : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:178
for d, b, a, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < d : ( ( real ) ( complex ext-real real ) number ) & d : ( ( real ) ( complex ext-real real ) number ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) < a : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) holds
((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) - d : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) * b : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) + (d : ( ( real ) ( complex ext-real real ) number ) * c : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:179
for d, a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= d : ( ( real ) ( complex ext-real real ) number ) & d : ( ( real ) ( complex ext-real real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) <= ((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) - d : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) * a : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) + (d : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) set ) & b : ( ( real ) ( complex ext-real real ) number ) < ((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) - d : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) * a : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) + (d : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) set ) holds
d : ( ( real ) ( complex ext-real real ) number ) = 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 ) ) ) ;

theorem :: XREAL_1:180
for d, a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= d : ( ( real ) ( complex ext-real real ) number ) & d : ( ( real ) ( complex ext-real real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) & ((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) - d : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) * a : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) + (d : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) & ((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) - d : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) * a : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) + (d : ( ( real ) ( complex ext-real real ) number ) * b : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) holds
d : ( ( real ) ( complex ext-real real ) number ) = 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 ) ) ) ;

begin

theorem :: XREAL_1:181
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) <= b : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:182
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) holds
1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) <= b : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:183
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: XREAL_1:184
for b, a being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: XREAL_1:185
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: XREAL_1:186
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: XREAL_1:187
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) holds
1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:188
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) < a : ( ( real ) ( complex ext-real real ) number ) holds
1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:189
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: XREAL_1:190
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) < a : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: XREAL_1:191
for a, b being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) < a : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: XREAL_1:192
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) < b : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;

begin

theorem :: XREAL_1:193
for b, a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= b : ( ( real ) ( complex ext-real real ) number ) & - b : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) holds
- 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:194
for b, a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= b : ( ( real ) ( complex ext-real real ) number ) & - a : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
- 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:195
for b, a being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) <= - b : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) holds
- 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:196
for b, a being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) <= 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) <= - a : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) holds
- 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:197
for b, a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & - b : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) holds
- 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:198
for b, a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & - a : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) holds
- 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:199
for b, a being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & a : ( ( real ) ( complex ext-real real ) number ) < - b : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) holds
- 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:200
for b, a being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & b : ( ( real ) ( complex ext-real real ) number ) < - a : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) holds
- 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:201
for b, a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) <= - b : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) ;

theorem :: XREAL_1:202
for b, a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) <= - a : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) ;

theorem :: XREAL_1:203
for b, a being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & - b : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) ;

theorem :: XREAL_1:204
for b, a being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & - a : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) <= b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) ;

theorem :: XREAL_1:205
for b, a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) < - b : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) ;

theorem :: XREAL_1:206
for b, a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < b : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) < - a : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) ;

theorem :: XREAL_1:207
for b, a being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & - b : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) ;

theorem :: XREAL_1:208
for b, a being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) < 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 ) ) ) & - a : ( ( real ) ( complex ext-real real ) number ) : ( ( complex ) ( complex ext-real real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) / b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) ;

begin

theorem :: XREAL_1:209
for c, b being ( ( real ) ( complex ext-real real ) number ) st ( for a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) holds
c : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ) holds
c : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:210
for b, c being ( ( real ) ( complex ext-real real ) number ) st ( for a being ( ( real ) ( complex ext-real real ) number ) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) / a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) ) holds
b : ( ( real ) ( complex ext-real real ) number ) <= c : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:211
for a being ( ( real ) ( complex ext-real real ) number ) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: XREAL_1:212
for a being ( ( real ) ( complex ext-real real ) number ) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: XREAL_1:213
for a being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) holds
- 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) <= a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:214
for a being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) < - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) holds
- 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( complex ) ( non empty complex ext-real non positive negative real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) " : ( ( complex ) ( complex ext-real real ) set ) ;

begin

theorem :: XREAL_1:215
for a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) holds
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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:216
for a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:217
for a being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty complex ext-real positive non negative real ) set ) holds
(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) * a : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) 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 ) ) ) ;

theorem :: XREAL_1:218
for a being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty complex ext-real positive non negative real ) set ) holds
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 ) ) ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) - (2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) * a : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:219
for a being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) >= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty complex ext-real positive non negative real ) set ) holds
(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) * a : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) 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 ) ) ) ;

theorem :: XREAL_1:220
for a being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) >= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty complex ext-real positive non negative real ) set ) holds
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 ) ) ) >= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) - (2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) * a : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) : ( ( ) ( complex ext-real real ) set ) ;

begin

theorem :: XREAL_1:221
for a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) / 3 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:222
for a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) holds
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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) / 3 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) set ) ;

begin

theorem :: XREAL_1:223
for a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) / 4 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:224
for a being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) holds
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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) / 4 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:225
for a, b being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) <> 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 ) ) ) holds
ex c being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) = b : ( ( real ) ( complex ext-real real ) number ) / c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

begin

theorem :: XREAL_1:226
for r, s being ( ( real ) ( complex ext-real real ) number ) st r : ( ( real ) ( complex ext-real real ) number ) < s : ( ( real ) ( complex ext-real real ) number ) holds
( r : ( ( real ) ( complex ext-real real ) number ) < (r : ( ( real ) ( complex ext-real real ) number ) + s : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) set ) & (r : ( ( real ) ( complex ext-real real ) number ) + s : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real real ) set ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real real ) set ) < s : ( ( real ) ( complex ext-real real ) number ) ) ;

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

theorem :: XREAL_1:227
for r, t being ( ( ext-real ) ( ext-real ) number ) st r : ( ( ext-real ) ( ext-real ) number ) < t : ( ( ext-real ) ( ext-real ) number ) holds
ex s being ( ( ext-real ) ( ext-real ) number ) st
( r : ( ( ext-real ) ( ext-real ) number ) < s : ( ( ext-real ) ( ext-real ) number ) & s : ( ( ext-real ) ( ext-real ) number ) < t : ( ( ext-real ) ( ext-real ) number ) ) ;

theorem :: XREAL_1:228
for r, s, t being ( ( ext-real ) ( ext-real ) number ) st r : ( ( ext-real ) ( ext-real ) number ) < s : ( ( ext-real ) ( ext-real ) number ) & ( for q being ( ( ext-real ) ( ext-real ) number ) st r : ( ( ext-real ) ( ext-real ) number ) < q : ( ( ext-real ) ( ext-real ) number ) & q : ( ( ext-real ) ( ext-real ) number ) < s : ( ( ext-real ) ( ext-real ) number ) holds
t : ( ( ext-real ) ( ext-real ) number ) <= q : ( ( ext-real ) ( ext-real ) number ) ) holds
t : ( ( ext-real ) ( ext-real ) number ) <= r : ( ( ext-real ) ( ext-real ) number ) ;

theorem :: XREAL_1:229
for r, s, t being ( ( ext-real ) ( ext-real ) number ) st r : ( ( ext-real ) ( ext-real ) number ) < s : ( ( ext-real ) ( ext-real ) number ) & ( for q being ( ( ext-real ) ( ext-real ) number ) st r : ( ( ext-real ) ( ext-real ) number ) < q : ( ( ext-real ) ( ext-real ) number ) & q : ( ( ext-real ) ( ext-real ) number ) < s : ( ( ext-real ) ( ext-real ) number ) holds
q : ( ( ext-real ) ( ext-real ) number ) <= t : ( ( ext-real ) ( ext-real ) number ) ) holds
s : ( ( ext-real ) ( ext-real ) number ) <= t : ( ( ext-real ) ( ext-real ) number ) ;

theorem :: XREAL_1:230
for a, b, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) <= c : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) <= c : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:231
for a, b, c being ( ( real ) ( complex ext-real real ) number ) st 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 ) ) ) < a : ( ( real ) ( complex ext-real real ) number ) & b : ( ( real ) ( complex ext-real real ) number ) <= c : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) - a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) < c : ( ( real ) ( complex ext-real real ) number ) ;

begin

theorem :: XREAL_1:232
for a being ( ( real ) ( complex ext-real real ) number ) holds a : ( ( real ) ( complex ext-real real ) number ) -' a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real non negative real ) 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 ) ) ) ;

theorem :: XREAL_1:233
for b, a being ( ( real ) ( complex ext-real real ) number ) st b : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) -' b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real non negative real ) set ) = a : ( ( real ) ( complex ext-real real ) number ) - b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) ;

theorem :: XREAL_1:234
for c, a, b being ( ( real ) ( complex ext-real real ) number ) st c : ( ( real ) ( complex ext-real real ) number ) <= a : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) & a : ( ( real ) ( complex ext-real real ) number ) -' c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real non negative real ) set ) = b : ( ( real ) ( complex ext-real real ) number ) -' c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real non negative real ) set ) holds
a : ( ( real ) ( complex ext-real real ) number ) = b : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:235
for a, b being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) >= b : ( ( real ) ( complex ext-real real ) number ) holds
(a : ( ( real ) ( complex ext-real real ) number ) -' b : ( ( real ) ( complex ext-real real ) number ) ) : ( ( ) ( complex ext-real non negative real ) set ) + b : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real real ) set ) = a : ( ( real ) ( complex ext-real real ) number ) ;

theorem :: XREAL_1:236
for a, b, c being ( ( real ) ( complex ext-real real ) number ) st a : ( ( real ) ( complex ext-real real ) number ) <= b : ( ( real ) ( complex ext-real real ) number ) & c : ( ( real ) ( complex ext-real real ) number ) < a : ( ( real ) ( complex ext-real real ) number ) holds
b : ( ( real ) ( complex ext-real real ) number ) -' a : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real non negative real ) set ) < b : ( ( real ) ( complex ext-real real ) number ) -' c : ( ( real ) ( complex ext-real real ) number ) : ( ( ) ( complex ext-real non negative real ) set ) ;

theorem :: XREAL_1:237
for a being ( ( real ) ( complex ext-real real ) number ) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) <= a : ( ( real ) ( complex ext-real real ) number ) holds
a : ( ( real ) ( complex ext-real real ) number ) -' 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ext-real non negative real ) set ) < a : ( ( real ) ( complex ext-real real ) number ) ;