:: BORSUK_5 semantic presentation

begin

theorem :: BORSUK_5:1
canceled;

theorem :: BORSUK_5:2
for x1, x2, x3, x4, x5, x6 being ( ( ) ( ) set ) holds {x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) = {x1 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) \/ {x2 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) : ( ( ) ( non empty V36() ) set ) ;

theorem :: BORSUK_5:3
for x1, x2, x3, x4, x5, x6 being ( ( ) ( ) set ) st x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) are_mutually_different holds
card {x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) : ( ( ) ( natural complex real ext-real V128() V129() V130() V131() V132() V133() integer non irrational ) Element of omega : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) set ) ) = 6 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BORSUK_5:4
for x1, x2, x3, x4, x5, x6, x7 being ( ( ) ( ) set ) st x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) ,x7 : ( ( ) ( ) set ) are_mutually_different holds
card {x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) ,x7 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) : ( ( ) ( natural complex real ext-real V128() V129() V130() V131() V132() V133() integer non irrational ) Element of omega : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) set ) ) = 7 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BORSUK_5:5
for x1, x2, x3, x4, x5, x6 being ( ( ) ( ) set ) st {x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) misses {x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) holds
( x1 : ( ( ) ( ) set ) <> x4 : ( ( ) ( ) set ) & x1 : ( ( ) ( ) set ) <> x5 : ( ( ) ( ) set ) & x1 : ( ( ) ( ) set ) <> x6 : ( ( ) ( ) set ) & x2 : ( ( ) ( ) set ) <> x4 : ( ( ) ( ) set ) & x2 : ( ( ) ( ) set ) <> x5 : ( ( ) ( ) set ) & x2 : ( ( ) ( ) set ) <> x6 : ( ( ) ( ) set ) & x3 : ( ( ) ( ) set ) <> x4 : ( ( ) ( ) set ) & x3 : ( ( ) ( ) set ) <> x5 : ( ( ) ( ) set ) & x3 : ( ( ) ( ) set ) <> x6 : ( ( ) ( ) set ) ) ;

theorem :: BORSUK_5:6
for x1, x2, x3, x4, x5, x6 being ( ( ) ( ) set ) st x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) are_mutually_different & x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) are_mutually_different & {x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) misses {x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) holds
x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) are_mutually_different ;

theorem :: BORSUK_5:7
for x1, x2, x3, x4, x5, x6, x7 being ( ( ) ( ) set ) st x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) are_mutually_different & {x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) misses {x7 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) holds
x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) ,x7 : ( ( ) ( ) set ) are_mutually_different ;

theorem :: BORSUK_5:8
for x1, x2, x3, x4, x5, x6, x7 being ( ( ) ( ) set ) st x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) ,x7 : ( ( ) ( ) set ) are_mutually_different holds
x7 : ( ( ) ( ) set ) ,x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) are_mutually_different ;

theorem :: BORSUK_5:9
for x1, x2, x3, x4, x5, x6, x7 being ( ( ) ( ) set ) st x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) ,x7 : ( ( ) ( ) set ) are_mutually_different holds
x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) ,x7 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) are_mutually_different ;

registration
cluster R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V127() ) TopStruct ) -> TopSpace-like pathwise_connected ;
end;

registration
cluster non empty TopSpace-like connected for ( ( ) ( ) TopStruct ) ;
end;

begin

theorem :: BORSUK_5:10
for A, B being ( ( ) ( V128() V129() V130() ) Subset of )
for a, b, c, d being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) & b : ( ( real ) ( complex real ext-real ) number ) <= c : ( ( real ) ( complex real ext-real ) number ) & c : ( ( real ) ( complex real ext-real ) number ) < d : ( ( real ) ( complex real ext-real ) number ) & A : ( ( ) ( V128() V129() V130() ) Subset of ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) & B : ( ( ) ( V128() V129() V130() ) Subset of ) = ].c : ( ( real ) ( complex real ext-real ) number ) ,d : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V128() V129() V130() ) Subset of ) ,B : ( ( ) ( V128() V129() V130() ) Subset of ) are_separated ;

theorem :: BORSUK_5:11
for a, b, c being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) <= c : ( ( real ) ( complex real ext-real ) number ) & c : ( ( real ) ( complex real ext-real ) number ) <= b : ( ( real ) ( complex real ext-real ) number ) holds
[.a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() closed ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ [.c : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:12
for a, b, c being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) <= c : ( ( real ) ( complex real ext-real ) number ) & c : ( ( real ) ( complex real ext-real ) number ) <= b : ( ( real ) ( complex real ext-real ) number ) holds
].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,c : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ [.a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() closed ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) = ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,b : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

registration
cluster -> real for ( ( ) ( ) Element of RAT : ( ( ) ( V128() V129() V130() V131() V134() ) set ) ) ;
end;

theorem :: BORSUK_5:13
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for p being ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V128() V129() V130() ) set ) ) holds
( p : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V128() V129() V130() ) set ) ) in Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) iff for r being ( ( real ) ( complex real ext-real ) number ) st r : ( ( real ) ( complex real ext-real ) number ) > 0 : ( ( ) ( empty natural complex real ext-real non positive non negative V36() V40() V128() V129() V130() V131() V132() V133() V134() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
Ball (p : ( ( ) ( complex real ext-real ) Point of ( ( ) ( non empty V128() V129() V130() ) set ) ) ,r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( V128() V129() V130() ) Element of bool the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning symmetric triangle Discerning V127() ) MetrStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) meets A : ( ( ) ( V128() V129() V130() ) Subset of ) ) ;

theorem :: BORSUK_5:14
for p, q being ( ( ) ( complex real ext-real ) Element of ( ( ) ( non empty V128() V129() V130() ) set ) ) st q : ( ( ) ( complex real ext-real ) Element of ( ( ) ( non empty V128() V129() V130() ) set ) ) >= p : ( ( ) ( complex real ext-real ) Element of ( ( ) ( non empty V128() V129() V130() ) set ) ) holds
dist (p : ( ( ) ( complex real ext-real ) Element of ( ( ) ( non empty V128() V129() V130() ) set ) ) ,q : ( ( ) ( complex real ext-real ) Element of ( ( ) ( non empty V128() V129() V130() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V128() V129() V130() V134() ) set ) ) = q : ( ( ) ( complex real ext-real ) Element of ( ( ) ( non empty V128() V129() V130() ) set ) ) - p : ( ( ) ( complex real ext-real ) Element of ( ( ) ( non empty V128() V129() V130() ) set ) ) : ( ( ) ( complex real ext-real ) set ) ;

theorem :: BORSUK_5:15
for A being ( ( ) ( V128() V129() V130() ) Subset of ) st A : ( ( ) ( V128() V129() V130() ) Subset of ) = RAT : ( ( ) ( V128() V129() V130() V131() V134() ) set ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) ;

theorem :: BORSUK_5:16
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a, b being ( ( real ) ( complex real ext-real ) number ) st A : ( ( ) ( V128() V129() V130() ) Subset of ) = ].a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( V128() V129() V130() open ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) & a : ( ( real ) ( complex real ext-real ) number ) <> b : ( ( real ) ( complex real ext-real ) number ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() closed ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

begin

registration
cluster number_e : ( ( real ) ( complex real ext-real ) set ) -> real irrational ;
end;

definition
func IRRAT -> ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) equals :: BORSUK_5:def 1
REAL : ( ( ) ( V128() V129() V130() V134() ) set ) \ RAT : ( ( ) ( V128() V129() V130() V131() V134() ) set ) : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let a, b be ( ( real ) ( complex real ext-real ) number ) ;
func RAT (a,b) -> ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) equals :: BORSUK_5:def 2
RAT : ( ( ) ( V128() V129() V130() V131() V134() ) set ) /\ ].a : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,b : ( ( ) ( ) Element of the carrier of a : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) .[ : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V128() V129() V130() V131() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;
func IRRAT (a,b) -> ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) equals :: BORSUK_5:def 3
IRRAT : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) /\ ].a : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,b : ( ( ) ( ) Element of the carrier of a : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) .[ : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: BORSUK_5:17
for x being ( ( real ) ( complex real ext-real ) number ) holds
( x : ( ( real ) ( complex real ext-real ) number ) is irrational iff x : ( ( real ) ( complex real ext-real ) number ) in IRRAT : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) ) ;

registration
cluster complex real ext-real irrational for ( ( ) ( ) set ) ;
end;

registration
cluster IRRAT : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) -> non empty ;
end;

registration
let a be ( ( rational ) ( complex real ext-real rational ) number ) ;
let b be ( ( real irrational ) ( complex real ext-real irrational ) number ) ;
cluster a : ( ( rational ) ( complex real ext-real rational ) set ) + b : ( ( real irrational ) ( complex real ext-real irrational ) set ) : ( ( ) ( complex real ext-real ) set ) -> irrational ;
cluster b : ( ( real irrational ) ( complex real ext-real irrational ) set ) + a : ( ( rational ) ( complex real ext-real rational ) set ) : ( ( ) ( complex real ext-real ) set ) -> irrational ;
end;

theorem :: BORSUK_5:18
for a being ( ( rational ) ( complex real ext-real rational ) number )
for b being ( ( real irrational ) ( complex real ext-real irrational ) number ) holds a : ( ( rational ) ( complex real ext-real rational ) number ) + b : ( ( real irrational ) ( complex real ext-real irrational ) number ) : ( ( ) ( complex real ext-real irrational ) set ) is irrational ;

registration
let a be ( ( real irrational ) ( complex real ext-real irrational ) number ) ;
cluster - a : ( ( real irrational ) ( complex real ext-real irrational ) set ) : ( ( complex ) ( complex real ext-real ) set ) -> complex irrational ;
end;

theorem :: BORSUK_5:19
for a being ( ( real irrational ) ( complex real ext-real irrational ) number ) holds - a : ( ( real irrational ) ( complex real ext-real irrational ) number ) : ( ( complex ) ( complex real ext-real irrational ) set ) is irrational ;

registration
let a be ( ( rational ) ( complex real ext-real rational ) number ) ;
let b be ( ( real irrational ) ( complex real ext-real irrational ) number ) ;
cluster a : ( ( rational ) ( complex real ext-real rational ) set ) - b : ( ( real irrational ) ( complex real ext-real irrational ) set ) : ( ( ) ( complex real ext-real ) set ) -> irrational ;
cluster b : ( ( real irrational ) ( complex real ext-real irrational ) set ) - a : ( ( rational ) ( complex real ext-real rational ) set ) : ( ( ) ( complex real ext-real ) set ) -> irrational ;
end;

theorem :: BORSUK_5:20
for a being ( ( rational ) ( complex real ext-real rational ) number )
for b being ( ( real irrational ) ( complex real ext-real irrational ) number ) holds a : ( ( rational ) ( complex real ext-real rational ) number ) - b : ( ( real irrational ) ( complex real ext-real irrational ) number ) : ( ( ) ( complex real ext-real irrational ) set ) is irrational ;

theorem :: BORSUK_5:21
for a being ( ( rational ) ( complex real ext-real rational ) number )
for b being ( ( real irrational ) ( complex real ext-real irrational ) number ) holds b : ( ( real irrational ) ( complex real ext-real irrational ) number ) - a : ( ( rational ) ( complex real ext-real rational ) number ) : ( ( ) ( complex real ext-real irrational ) set ) is irrational ;

theorem :: BORSUK_5:22
for a being ( ( rational ) ( complex real ext-real rational ) number )
for b being ( ( real irrational ) ( complex real ext-real irrational ) number ) st a : ( ( rational ) ( complex real ext-real rational ) number ) <> 0 : ( ( ) ( empty natural complex real ext-real non positive non negative V36() V40() V128() V129() V130() V131() V132() V133() V134() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
a : ( ( rational ) ( complex real ext-real rational ) number ) * b : ( ( real irrational ) ( complex real ext-real irrational ) number ) : ( ( ) ( complex real ext-real ) set ) is irrational ;

theorem :: BORSUK_5:23
for a being ( ( rational ) ( complex real ext-real rational ) number )
for b being ( ( real irrational ) ( complex real ext-real irrational ) number ) st a : ( ( rational ) ( complex real ext-real rational ) number ) <> 0 : ( ( ) ( empty natural complex real ext-real non positive non negative V36() V40() V128() V129() V130() V131() V132() V133() V134() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
b : ( ( real irrational ) ( complex real ext-real irrational ) number ) / a : ( ( rational ) ( complex real ext-real rational ) number ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( V128() V134() ) set ) ) is irrational ;

registration
cluster real irrational -> non zero real for ( ( ) ( ) set ) ;
end;

theorem :: BORSUK_5:24
for a being ( ( rational ) ( complex real ext-real rational ) number )
for b being ( ( real irrational ) ( non zero complex real ext-real irrational ) number ) st a : ( ( rational ) ( complex real ext-real rational ) number ) <> 0 : ( ( ) ( empty natural complex real ext-real non positive non negative V36() V40() V128() V129() V130() V131() V132() V133() V134() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
a : ( ( rational ) ( complex real ext-real rational ) number ) / b : ( ( real irrational ) ( non zero complex real ext-real irrational ) number ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( V128() V134() ) set ) ) is irrational ;

registration
let r be ( ( real irrational ) ( non zero complex real ext-real irrational ) number ) ;
cluster frac r : ( ( real irrational ) ( non zero complex real ext-real irrational ) set ) : ( ( ) ( complex real ext-real ) set ) -> irrational ;
end;

theorem :: BORSUK_5:25
for r being ( ( real irrational ) ( non zero complex real ext-real irrational ) number ) holds frac r : ( ( real irrational ) ( non zero complex real ext-real irrational ) number ) : ( ( ) ( non zero complex real ext-real irrational ) Element of REAL : ( ( ) ( V128() V129() V130() V134() ) set ) ) is irrational ;

registration
cluster non zero complex real ext-real rational for ( ( ) ( ) set ) ;
end;

registration
let a be ( ( non zero rational ) ( non zero complex real ext-real rational ) number ) ;
let b be ( ( real irrational ) ( non zero complex real ext-real irrational ) number ) ;
cluster a : ( ( non zero rational ) ( non zero complex real ext-real rational ) set ) * b : ( ( real irrational ) ( non zero complex real ext-real irrational ) set ) : ( ( ) ( complex real ext-real ) set ) -> irrational ;
cluster b : ( ( real irrational ) ( non zero complex real ext-real irrational ) set ) * a : ( ( non zero rational ) ( non zero complex real ext-real rational ) set ) : ( ( ) ( complex real ext-real ) set ) -> irrational ;
cluster a : ( ( non zero rational ) ( non zero complex real ext-real rational ) set ) / b : ( ( real irrational ) ( non zero complex real ext-real irrational ) set ) : ( ( ) ( complex real ext-real ) set ) -> irrational ;
cluster b : ( ( real irrational ) ( non zero complex real ext-real irrational ) set ) / a : ( ( non zero rational ) ( non zero complex real ext-real rational ) set ) : ( ( ) ( complex real ext-real ) set ) -> irrational ;
end;

theorem :: BORSUK_5:26
for a, b being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) holds
ex p1, p2 being ( ( rational ) ( complex real ext-real rational ) number ) st
( a : ( ( real ) ( complex real ext-real ) number ) < p1 : ( ( rational ) ( complex real ext-real rational ) number ) & p1 : ( ( rational ) ( complex real ext-real rational ) number ) < p2 : ( ( rational ) ( complex real ext-real rational ) number ) & p2 : ( ( rational ) ( complex real ext-real rational ) number ) < b : ( ( real ) ( complex real ext-real ) number ) ) ;

theorem :: BORSUK_5:27
for a, b being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) holds
ex p being ( ( real irrational ) ( non zero complex real ext-real irrational ) number ) st
( a : ( ( real ) ( complex real ext-real ) number ) < p : ( ( real irrational ) ( non zero complex real ext-real irrational ) number ) & p : ( ( real irrational ) ( non zero complex real ext-real irrational ) number ) < b : ( ( real ) ( complex real ext-real ) number ) ) ;

theorem :: BORSUK_5:28
for A being ( ( ) ( V128() V129() V130() ) Subset of ) st A : ( ( ) ( V128() V129() V130() ) Subset of ) = IRRAT : ( ( ) ( non empty V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) ;

theorem :: BORSUK_5:29
for a, b, c being ( ( real ) ( complex real ext-real ) number ) holds
( c : ( ( real ) ( complex real ext-real ) number ) in RAT (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) iff ( c : ( ( real ) ( complex real ext-real ) number ) is rational & a : ( ( real ) ( complex real ext-real ) number ) < c : ( ( real ) ( complex real ext-real ) number ) & c : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) ) ) ;

theorem :: BORSUK_5:30
for a, b, c being ( ( real ) ( complex real ext-real ) number ) holds
( c : ( ( real ) ( complex real ext-real ) number ) in IRRAT (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) iff ( c : ( ( real ) ( complex real ext-real ) number ) is irrational & a : ( ( real ) ( complex real ext-real ) number ) < c : ( ( real ) ( complex real ext-real ) number ) & c : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) ) ) ;

theorem :: BORSUK_5:31
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a, b being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) & A : ( ( ) ( V128() V129() V130() ) Subset of ) = RAT (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() closed ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:32
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a, b being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) & A : ( ( ) ( V128() V129() V130() ) Subset of ) = IRRAT (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() closed ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:33
for T being ( ( TopSpace-like connected ) ( TopSpace-like connected ) TopSpace)
for A being ( ( open closed ) ( open closed ) Subset of ) holds
( A : ( ( open closed ) ( open closed ) Subset of ) = {} : ( ( ) ( empty V36() V40() V128() V129() V130() V131() V132() V133() V134() ) set ) or A : ( ( open closed ) ( open closed ) Subset of ) = [#] T : ( ( TopSpace-like connected ) ( TopSpace-like connected ) TopSpace) : ( ( ) ( non proper open closed ) Element of bool the carrier of b1 : ( ( TopSpace-like connected ) ( TopSpace-like connected ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BORSUK_5:34
for A being ( ( ) ( V128() V129() V130() ) Subset of ) st A : ( ( ) ( V128() V129() V130() ) Subset of ) is closed & A : ( ( ) ( V128() V129() V130() ) Subset of ) is open & not A : ( ( ) ( V128() V129() V130() ) Subset of ) = {} : ( ( ) ( empty V36() V40() V128() V129() V130() V131() V132() V133() V134() ) set ) holds
A : ( ( ) ( V128() V129() V130() ) Subset of ) = REAL : ( ( ) ( V128() V129() V130() V134() ) set ) ;

begin

theorem :: BORSUK_5:35
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a, b being ( ( real ) ( complex real ext-real ) number ) st A : ( ( ) ( V128() V129() V130() ) Subset of ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) & a : ( ( real ) ( complex real ext-real ) number ) <> b : ( ( real ) ( complex real ext-real ) number ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() closed ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:36
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a, b being ( ( real ) ( complex real ext-real ) number ) st A : ( ( ) ( V128() V129() V130() ) Subset of ) = ].a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) & a : ( ( real ) ( complex real ext-real ) number ) <> b : ( ( real ) ( complex real ext-real ) number ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() closed ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:37
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a, b, c being ( ( real ) ( complex real ext-real ) number ) st A : ( ( ) ( V128() V129() V130() ) Subset of ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) & a : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) & b : ( ( real ) ( complex real ext-real ) number ) < c : ( ( real ) ( complex real ext-real ) number ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() closed ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:38
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a being ( ( real ) ( complex real ext-real ) number ) st A : ( ( ) ( V128() V129() V130() ) Subset of ) = {a : ( ( real ) ( complex real ext-real ) number ) } : ( ( ) ( non empty V36() V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = {a : ( ( real ) ( complex real ext-real ) number ) } : ( ( ) ( non empty V36() V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:39
for A being ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) )
for B being ( ( ) ( V128() V129() V130() ) Subset of ) st A : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) = B : ( ( ) ( V128() V129() V130() ) Subset of ) holds
( A : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) is open iff B : ( ( ) ( V128() V129() V130() ) Subset of ) is open ) ;

registration
let A, B be ( ( open ) ( V128() V129() V130() open ) Subset of ( ( ) ( non empty ) set ) ) ;
cluster A : ( ( open ) ( V128() V129() V130() open ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) /\ B : ( ( open ) ( V128() V129() V130() open ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V128() V129() V130() ) set ) -> open for ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) ;
cluster A : ( ( open ) ( V128() V129() V130() open ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ B : ( ( open ) ( V128() V129() V130() open ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V128() V129() V130() ) set ) -> open for ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) ;
end;

theorem :: BORSUK_5:40
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a, b being ( ( ext-real ) ( ext-real ) number ) st A : ( ( ) ( V128() V129() V130() ) Subset of ) = ].a : ( ( ext-real ) ( ext-real ) number ) ,b : ( ( ext-real ) ( ext-real ) number ) .[ : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V128() V129() V130() ) Subset of ) is open ;

theorem :: BORSUK_5:41
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a being ( ( real ) ( complex real ext-real ) number ) st A : ( ( ) ( V128() V129() V130() ) Subset of ) = ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V128() V129() V130() ) Subset of ) is closed ;

theorem :: BORSUK_5:42
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a being ( ( real ) ( complex real ext-real ) number ) st A : ( ( ) ( V128() V129() V130() ) Subset of ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V128() V129() V130() ) Subset of ) is closed ;

theorem :: BORSUK_5:43
for a being ( ( real ) ( complex real ext-real ) number ) holds [.a : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) = {a : ( ( real ) ( complex real ext-real ) number ) } : ( ( ) ( non empty V36() V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].a : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:44
for a being ( ( real ) ( complex real ext-real ) number ) holds ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) = {a : ( ( real ) ( complex real ext-real ) number ) } : ( ( ) ( non empty V36() V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

registration
let a be ( ( real ) ( complex real ext-real ) number ) ;
cluster K451(a : ( ( real ) ( complex real ext-real ) set ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster K450(-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster K451(-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster K449(a : ( ( real ) ( complex real ext-real ) set ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) ) : ( ( ) ( ) set ) -> non empty ;
end;

theorem :: BORSUK_5:45
for a being ( ( real ) ( complex real ext-real ) number ) holds ].a : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) <> REAL : ( ( ) ( V128() V129() V130() V134() ) set ) ;

theorem :: BORSUK_5:46
for a being ( ( real ) ( complex real ext-real ) number ) holds [.a : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) <> REAL : ( ( ) ( V128() V129() V130() V134() ) set ) ;

theorem :: BORSUK_5:47
for a being ( ( real ) ( complex real ext-real ) number ) holds ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) <> REAL : ( ( ) ( V128() V129() V130() V134() ) set ) ;

theorem :: BORSUK_5:48
for a being ( ( real ) ( complex real ext-real ) number ) holds ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) <> REAL : ( ( ) ( V128() V129() V130() V134() ) set ) ;

theorem :: BORSUK_5:49
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a being ( ( real ) ( complex real ext-real ) number ) st A : ( ( ) ( V128() V129() V130() ) Subset of ) = ].a : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:50
for a being ( ( real ) ( complex real ext-real ) number ) holds Cl ].a : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:51
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a being ( ( real ) ( complex real ext-real ) number ) st A : ( ( ) ( V128() V129() V130() ) Subset of ) = ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:52
for a being ( ( real ) ( complex real ext-real ) number ) holds Cl ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) = ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:53
for A, B being ( ( ) ( V128() V129() V130() ) Subset of )
for b being ( ( real ) ( complex real ext-real ) number ) st A : ( ( ) ( V128() V129() V130() ) Subset of ) = ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,b : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) & B : ( ( ) ( V128() V129() V130() ) Subset of ) = ].b : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V128() V129() V130() ) Subset of ) ,B : ( ( ) ( V128() V129() V130() ) Subset of ) are_separated ;

theorem :: BORSUK_5:54
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a, b being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) & A : ( ( ) ( V128() V129() V130() ) Subset of ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].b : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:55
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a, b being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) & A : ( ( ) ( V128() V129() V130() ) Subset of ) = ].a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( V128() V129() V130() open ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].b : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:56
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a, b, c being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) & b : ( ( real ) ( complex real ext-real ) number ) < c : ( ( real ) ( complex real ext-real ) number ) & A : ( ( ) ( V128() V129() V130() ) Subset of ) = ((RAT (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) )) : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) \/ ].b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( V128() V129() V130() open ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].c : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:57
for a, b being ( ( real ) ( complex real ext-real ) number ) holds IRRAT (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) misses RAT (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:58
for a, b being ( ( real ) ( complex real ext-real ) number ) holds REAL : ( ( ) ( V128() V129() V130() V134() ) set ) \ (RAT (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) )) : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) = (].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ (IRRAT (a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) )) : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ [.b : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:59
for a, b being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) holds
[.a : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \ (].a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( V128() V129() V130() open ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].b : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) = {a : ( ( real ) ( complex real ext-real ) number ) } : ( ( ) ( non empty V36() V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ {b : ( ( real ) ( complex real ext-real ) number ) } : ( ( ) ( non empty V36() V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V36() V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:60
for A being ( ( ) ( V128() V129() V130() ) Subset of ) st A : ( ( ) ( V128() V129() V130() ) Subset of ) = ((RAT (2 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) ,4 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) \/ ].4 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) ,5 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) .[ : ( ( ) ( V128() V129() V130() open ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].5 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V128() V129() V130() ) Subset of ) ` : ( ( ) ( V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = ((].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,2 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) .] : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ (IRRAT (2 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) ,4 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ {4 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty V36() V128() V129() V130() V131() V132() V133() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ {5 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty V36() V128() V129() V130() V131() V132() V133() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:61
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a being ( ( real ) ( complex real ext-real ) number ) st A : ( ( ) ( V128() V129() V130() ) Subset of ) = {a : ( ( real ) ( complex real ext-real ) number ) } : ( ( ) ( non empty V36() V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V128() V129() V130() ) Subset of ) ` : ( ( ) ( V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].a : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:62
(].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,1 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].1 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) /\ (((].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,2 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) .] : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ (IRRAT (2 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) ,4 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ {4 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty V36() V128() V129() V130() V131() V132() V133() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ {5 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty V36() V128() V129() V130() V131() V132() V133() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) = (((].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,1 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].1 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) .] : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ (IRRAT (2 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) ,4 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ {4 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty V36() V128() V129() V130() V131() V132() V133() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ {5 : ( ( ) ( non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational ) Element of NAT : ( ( ) ( V128() V129() V130() V131() V132() V133() V134() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty V36() V128() V129() V130() V131() V132() V133() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:63
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a, b being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) <= b : ( ( real ) ( complex real ext-real ) number ) & A : ( ( ) ( V128() V129() V130() ) Subset of ) = {a : ( ( real ) ( complex real ext-real ) number ) } : ( ( ) ( non empty V36() V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ [.b : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V128() V129() V130() ) Subset of ) ` : ( ( ) ( V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( V128() V129() V130() open ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:64
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a, b being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) & A : ( ( ) ( V128() V129() V130() ) Subset of ) = ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( V128() V129() V130() open ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,b : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:65
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a, b being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) & A : ( ( ) ( V128() V129() V130() ) Subset of ) = ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,b : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:66
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a, b, c being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) & b : ( ( real ) ( complex real ext-real ) number ) < c : ( ( real ) ( complex real ext-real ) number ) & A : ( ( ) ( V128() V129() V130() ) Subset of ) = ((].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ (IRRAT (b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) )) : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ {c : ( ( real ) ( complex real ext-real ) number ) } : ( ( ) ( non empty V36() V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,c : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:67
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a, b, c, d being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) & b : ( ( real ) ( complex real ext-real ) number ) < c : ( ( real ) ( complex real ext-real ) number ) & A : ( ( ) ( V128() V129() V130() ) Subset of ) = (((].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ (IRRAT (b : ( ( real ) ( complex real ext-real ) number ) ,c : ( ( real ) ( complex real ext-real ) number ) )) : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ {c : ( ( real ) ( complex real ext-real ) number ) } : ( ( ) ( non empty V36() V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ {d : ( ( real ) ( complex real ext-real ) number ) } : ( ( ) ( non empty V36() V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
Cl A : ( ( ) ( V128() V129() V130() ) Subset of ) : ( ( ) ( closed V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,c : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ {d : ( ( real ) ( complex real ext-real ) number ) } : ( ( ) ( non empty V36() V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:68
for A being ( ( ) ( V128() V129() V130() ) Subset of )
for a, b being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) <= b : ( ( real ) ( complex real ext-real ) number ) & A : ( ( ) ( V128() V129() V130() ) Subset of ) = ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ {b : ( ( real ) ( complex real ext-real ) number ) } : ( ( ) ( non empty V36() V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V128() V129() V130() ) Subset of ) ` : ( ( ) ( V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) = ].a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .[ : ( ( ) ( V128() V129() V130() open ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ ].b : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:69
for a, b being ( ( real ) ( complex real ext-real ) number ) holds [.a : ( ( real ) ( complex real ext-real ) number ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ {b : ( ( real ) ( complex real ext-real ) number ) } : ( ( ) ( non empty V36() V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) <> REAL : ( ( ) ( V128() V129() V130() V134() ) set ) ;

theorem :: BORSUK_5:70
for a, b being ( ( real ) ( complex real ext-real ) number ) holds ].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,a : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) \/ {b : ( ( real ) ( complex real ext-real ) number ) } : ( ( ) ( non empty V36() V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V128() V129() V130() ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) <> REAL : ( ( ) ( V128() V129() V130() V134() ) set ) ;

theorem :: BORSUK_5:71
for TS being ( ( ) ( ) TopStruct )
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) <> B : ( ( ) ( ) Subset of ) holds
A : ( ( ) ( ) Subset of ) ` : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) <> B : ( ( ) ( ) Subset of ) ` : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:72
for A being ( ( ) ( V128() V129() V130() ) Subset of ) st REAL : ( ( ) ( V128() V129() V130() V134() ) set ) = A : ( ( ) ( V128() V129() V130() ) Subset of ) ` : ( ( ) ( V128() V129() V130() ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected V127() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V128() V129() V130() ) set ) : ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V128() V129() V130() ) Subset of ) = {} : ( ( ) ( empty V36() V40() V128() V129() V130() V131() V132() V133() V134() ) set ) ;

begin

theorem :: BORSUK_5:73
for X being ( ( compact ) ( compact V128() V129() V130() ) Subset of )
for X9 being ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) st X9 : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) = X : ( ( compact ) ( compact V128() V129() V130() ) Subset of ) holds
( X9 : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) is bounded_above & X9 : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) is bounded_below ) ;

theorem :: BORSUK_5:74
for X being ( ( compact ) ( compact V128() V129() V130() ) Subset of )
for X9 being ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) )
for x being ( ( real ) ( complex real ext-real ) number ) st x : ( ( real ) ( complex real ext-real ) number ) in X9 : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) & X9 : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) = X : ( ( compact ) ( compact V128() V129() V130() ) Subset of ) holds
( lower_bound X9 : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V128() V129() V130() V134() ) set ) ) <= x : ( ( real ) ( complex real ext-real ) number ) & x : ( ( real ) ( complex real ext-real ) number ) <= upper_bound X9 : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V128() V129() V130() V134() ) set ) ) ) ;

theorem :: BORSUK_5:75
for C being ( ( non empty connected compact ) ( non empty connected compact V128() V129() V130() ) Subset of )
for C9 being ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) st C : ( ( non empty connected compact ) ( non empty connected compact V128() V129() V130() ) Subset of ) = C9 : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) & [.(lower_bound C9 : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V128() V129() V130() V134() ) set ) ) ,(upper_bound C9 : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V128() V129() V130() V134() ) set ) ) .] : ( ( ) ( V128() V129() V130() closed ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) c= C9 : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) holds
[.(lower_bound C9 : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V128() V129() V130() V134() ) set ) ) ,(upper_bound C9 : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V128() V129() V130() V134() ) set ) ) .] : ( ( ) ( V128() V129() V130() closed ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) = C9 : ( ( ) ( V128() V129() V130() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:76
for A being ( ( connected ) ( connected V128() V129() V130() ) Subset of )
for a, b, c being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) <= b : ( ( real ) ( complex real ext-real ) number ) & b : ( ( real ) ( complex real ext-real ) number ) <= c : ( ( real ) ( complex real ext-real ) number ) & a : ( ( real ) ( complex real ext-real ) number ) in A : ( ( connected ) ( connected V128() V129() V130() ) Subset of ) & c : ( ( real ) ( complex real ext-real ) number ) in A : ( ( connected ) ( connected V128() V129() V130() ) Subset of ) holds
b : ( ( real ) ( complex real ext-real ) number ) in A : ( ( connected ) ( connected V128() V129() V130() ) Subset of ) ;

theorem :: BORSUK_5:77
for A being ( ( connected ) ( connected V128() V129() V130() ) Subset of )
for a, b being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) in A : ( ( connected ) ( connected V128() V129() V130() ) Subset of ) & b : ( ( real ) ( complex real ext-real ) number ) in A : ( ( connected ) ( connected V128() V129() V130() ) Subset of ) holds
[.a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() closed ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) c= A : ( ( connected ) ( connected V128() V129() V130() ) Subset of ) ;

theorem :: BORSUK_5:78
for X being ( ( non empty connected compact ) ( non empty connected compact V128() V129() V130() ) Subset of ) holds X : ( ( non empty connected compact ) ( non empty connected compact V128() V129() V130() ) Subset of ) is ( ( non empty closed_interval ) ( non empty V128() V129() V130() closed_interval interval ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: BORSUK_5:79
for A being ( ( non empty connected compact ) ( non empty connected compact V128() V129() V130() ) Subset of ) ex a, b being ( ( real ) ( complex real ext-real ) number ) st
( a : ( ( real ) ( complex real ext-real ) number ) <= b : ( ( real ) ( complex real ext-real ) number ) & A : ( ( non empty connected compact ) ( non empty connected compact V128() V129() V130() ) Subset of ) = [.a : ( ( real ) ( complex real ext-real ) number ) ,b : ( ( real ) ( complex real ext-real ) number ) .] : ( ( ) ( V128() V129() V130() closed ) Element of bool REAL : ( ( ) ( V128() V129() V130() V134() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

registration
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
cluster non empty open closed for ( ( ) ( ) Element of bool (bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;