:: TREAL_1 semantic presentation

begin

theorem :: TREAL_1:1
for a, b being ( ( real ) ( V11() real ext-real ) number )
for A being ( ( ) ( V45() V46() V47() ) Subset of ) st A : ( ( ) ( V45() V46() V47() ) Subset of ) = [.a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) .] : ( ( ) ( V45() V46() V47() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) holds
A : ( ( ) ( V45() V46() V47() ) Subset of ) is closed ;

theorem :: TREAL_1:2
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) holds
Closed-Interval-TSpace (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) is closed ;

theorem :: TREAL_1:3
for a, c, d, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) <= c : ( ( real ) ( V11() real ext-real ) number ) & d : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) & c : ( ( real ) ( V11() real ext-real ) number ) <= d : ( ( real ) ( V11() real ext-real ) number ) holds
Closed-Interval-TSpace (c : ( ( real ) ( V11() real ext-real ) number ) ,d : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) is ( ( closed ) ( TopSpace-like closed V146() ) SubSpace of Closed-Interval-TSpace (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) ) ;

theorem :: TREAL_1:4
for a, c, b, d being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) <= c : ( ( real ) ( V11() real ext-real ) number ) & b : ( ( real ) ( V11() real ext-real ) number ) <= d : ( ( real ) ( V11() real ext-real ) number ) & c : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) holds
( Closed-Interval-TSpace (a : ( ( real ) ( V11() real ext-real ) number ) ,d : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) = (Closed-Interval-TSpace (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) union (Closed-Interval-TSpace (c : ( ( real ) ( V11() real ext-real ) number ) ,d : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) & Closed-Interval-TSpace (c : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) = (Closed-Interval-TSpace (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) meet (Closed-Interval-TSpace (c : ( ( real ) ( V11() real ext-real ) number ) ,d : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) ) ;

definition
let a, b be ( ( real ) ( V11() real ext-real ) number ) ;
assume a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) ;
func (#) (a,b) -> ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) equals :: TREAL_1:def 1
a : ( ( ) ( ) 2-sorted ) ;
func (a,b) (#) -> ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) equals :: TREAL_1:def 2
b : ( ( ) ( ) set ) ;
end;

theorem :: TREAL_1:5
( 0[01] : ( ( ) ( V11() real ext-real ) Element of the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V146() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) = (#) (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) & 1[01] : ( ( ) ( V11() real ext-real ) Element of the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V146() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) = (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) (#) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) ;

theorem :: TREAL_1:6
for a, b, c being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) & b : ( ( real ) ( V11() real ext-real ) number ) <= c : ( ( real ) ( V11() real ext-real ) number ) holds
( (#) (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) = (#) (a : ( ( real ) ( V11() real ext-real ) number ) ,c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) & (b : ( ( real ) ( V11() real ext-real ) number ) ,c : ( ( real ) ( V11() real ext-real ) number ) ) (#) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) = (a : ( ( real ) ( V11() real ext-real ) number ) ,c : ( ( real ) ( V11() real ext-real ) number ) ) (#) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) ;

begin

definition
let a, b be ( ( real ) ( V11() real ext-real ) number ) ;
assume a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) ;
let t1, t2 be ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ;
func L[01] (t1,t2) -> ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (a : ( ( ) ( ) 2-sorted ) ,b : ( ( ) ( ) set ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) means :: TREAL_1:def 3
 for s being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) holds it : ( ( ) ( ) M18(b : ( ( ) ( ) set ) ,t1 : ( ( ) ( ) Element of a : ( ( ) ( ) 2-sorted ) ) )) . s : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of (Closed-Interval-TSpace (a : ( ( ) ( ) 2-sorted ) ,b : ( ( ) ( ) set ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) = ((1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) - s : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * t1 : ( ( ) ( ) Element of a : ( ( ) ( ) 2-sorted ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) + (s : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) * t2 : ( ( ) ( ) Element of the carrier of b : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ;
end;

theorem :: TREAL_1:7
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) holds
for t1, t2 being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) )
for s being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) holds (L[01] (t1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,t2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . s : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) = ((t2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) - t1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) * s : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) + t1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: TREAL_1:8
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) holds
for t1, t2 being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) holds L[01] (t1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,t2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is continuous ;

theorem :: TREAL_1:9
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) holds
for t1, t2 being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) holds
( (L[01] (t1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,t2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . ((#) (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) = t1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) & (L[01] (t1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,t2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . ((0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) = t2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) ;

theorem :: TREAL_1:10
L[01] (((#) (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) = id (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Element of K6(K7( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) , the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

definition
let a, b be ( ( real ) ( V11() real ext-real ) number ) ;
assume a : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) ;
let t1, t2 be ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ;
func P[01] (a,b,t1,t2) -> ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (a : ( ( ) ( ) 2-sorted ) ,b : ( ( ) ( ) set ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (a : ( ( ) ( ) 2-sorted ) ,b : ( ( ) ( ) set ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) means :: TREAL_1:def 4
 for s being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) holds it : ( ( ) ( ) M18(b : ( ( ) ( ) set ) ,t1 : ( ( ) ( ) Element of a : ( ( ) ( ) 2-sorted ) ) )) . s : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) = (((b : ( ( ) ( ) set ) - s : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( ) ( ) set ) * t1 : ( ( ) ( ) Element of a : ( ( ) ( ) 2-sorted ) ) ) : ( ( ) ( ) set ) + ((s : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) - a : ( ( ) ( ) 2-sorted ) ) : ( ( ) ( ) set ) * t2 : ( ( ) ( ) Element of the carrier of b : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) / (b : ( ( ) ( ) set ) - a : ( ( ) ( ) 2-sorted ) ) : ( ( ) ( ) set ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ) ;
end;

theorem :: TREAL_1:11
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) holds
for t1, t2 being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) )
for s being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) holds (P[01] (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,t1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,t2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . s : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) = (((t2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) - t1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) / (b : ( ( real ) ( V11() real ext-real ) number ) - a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ) * s : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) + (((b : ( ( real ) ( V11() real ext-real ) number ) * t1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) - (a : ( ( real ) ( V11() real ext-real ) number ) * t2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / (b : ( ( real ) ( V11() real ext-real ) number ) - a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: TREAL_1:12
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) holds
for t1, t2 being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) holds P[01] (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,t1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,t2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is continuous ;

theorem :: TREAL_1:13
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) holds
for t1, t2 being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) holds
( (P[01] (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,t1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,t2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . ((#) (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) = t1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) & (P[01] (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,t1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,t2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . ((a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) = t2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) ;

theorem :: TREAL_1:14
P[01] (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,((#) (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) = id (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Element of K6(K7( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) , the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: TREAL_1:15
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) holds
( id (Closed-Interval-TSpace (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Element of K6(K7( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) , the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = (L[01] (((#) (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) * (P[01] (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,((#) (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( Function-like ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Element of K6(K7( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) , the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & id (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Element of K6(K7( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) , the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = (P[01] (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,((#) (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) * (L[01] (((#) (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( Function-like ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Element of K6(K7( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) , the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: TREAL_1:16
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) holds
( id (Closed-Interval-TSpace (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Element of K6(K7( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) , the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = (L[01] (((a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((#) (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) * (P[01] (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,((0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((#) (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( Function-like ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Element of K6(K7( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) , the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & id (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Element of K6(K7( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) , the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = (P[01] (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,((0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((#) (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) * (L[01] (((a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((#) (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( Function-like ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Element of K6(K7( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) , the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: TREAL_1:17
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) holds
( L[01] (((#) (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is being_homeomorphism & (L[01] (((#) (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) " : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Element of K6(K7( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) , the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = P[01] (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,((#) (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) & P[01] (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,((#) (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is being_homeomorphism & (P[01] (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,((#) (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) " : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Element of K6(K7( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) , the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = L[01] (((#) (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) ) ;

theorem :: TREAL_1:18
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) holds
( L[01] (((a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((#) (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is being_homeomorphism & (L[01] (((a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((#) (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) " : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Element of K6(K7( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) , the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = P[01] (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,((0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((#) (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) & P[01] (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,((0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((#) (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is being_homeomorphism & (P[01] (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ,((0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((#) (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) " : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Element of K6(K7( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) , the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = L[01] (((a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) (#)) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,((#) (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) ) ;

begin

theorem :: TREAL_1:19
I[01] : ( ( ) ( non empty strict TopSpace-like V146() ) TopStruct ) is connected ;

theorem :: TREAL_1:20
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) holds
Closed-Interval-TSpace (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) is connected ;

theorem :: TREAL_1:21
for f being ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V146() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V146() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V146() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) ex x being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) st f : ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V146() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V146() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V146() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V146() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) = x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ;

theorem :: TREAL_1:22
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) holds
for f being ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) ex x being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) st f : ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) = x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ;

theorem :: TREAL_1:23
for X, Y being ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) )
for f being ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of b1 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) st ex a, b being ( ( ) ( V11() real ext-real ) Real) st
( a : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) <= b : ( ( ) ( V11() real ext-real ) Real) & [.a : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,b : ( ( ) ( V11() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) c= the carrier of X : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) & [.a : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,b : ( ( ) ( V11() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) c= the carrier of Y : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) & f : ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of b1 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) .: [.a : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,b : ( ( ) ( V11() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of K6( the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( ) set ) ) c= [.a : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,b : ( ( ) ( V11() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) holds
ex x being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) st f : ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of b1 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) = x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ;

theorem :: TREAL_1:24
for X, Y being ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) )
for f being ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of b1 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) st ex a, b being ( ( ) ( V11() real ext-real ) Real) st
( a : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) <= b : ( ( ) ( V11() real ext-real ) Real) & [.a : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,b : ( ( ) ( V11() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) c= the carrier of X : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) & f : ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of b1 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) .: [.a : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,b : ( ( ) ( V11() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of K6( the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( ) set ) ) c= [.a : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ,b : ( ( ) ( V11() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() ) Element of K6(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) holds
ex x being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) st f : ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of b1 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) V20( the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like V146() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V146() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) = x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) ;