BROUWER

:: BROUWER semantic presentation

begin

definition

let S, T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;

func DiffElems (S,T) -> ( ( ) ( ) Subset of ) equals :: BROUWER:def 1
{ [s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( non empty ) Element of the carrier of [:S : ( ( ) ( ) TopStruct ) ,T : ( ( ) ( ) Element of bool (bool S : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) where s is ( ( ) ( ) Point of ( ( ) ( ) set ) ) , t is ( ( ) ( ) Point of ( ( ) ( ) set ) ) : s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) <> t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) } ;

end;

theorem :: BROUWER:1

for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in DiffElems (S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) Subset of ) iff ex s being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ex t being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st
( x : ( ( ) ( ) set ) = [s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( non empty ) Element of the carrier of [:b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) & s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) <> t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) ;

registration

let S be ( ( non trivial TopSpace-like ) ( non empty non trivial TopSpace-like ) TopSpace) ;
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;

cluster DiffElems (S : ( ( non trivial TopSpace-like ) ( non empty non trivial TopSpace-like ) TopStruct ) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( ) Subset of ) -> non empty ;

end;

registration

let S be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let T be ( ( non trivial TopSpace-like ) ( non empty non trivial TopSpace-like ) TopSpace) ;

cluster DiffElems (S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,T : ( ( non trivial TopSpace-like ) ( non empty non trivial TopSpace-like ) TopStruct ) ) : ( ( ) ( ) Subset of ) -> non empty ;

end;

theorem :: BROUWER:2

definition

let n be ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
let x be ( ( ) ( V16() Function-like V50(n : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ;
let r be ( ( real ) ( V11() ext-real real ) number ) ;

func Tdisk (x,r) -> ( ( ) ( TopSpace-like ) SubSpace of TOP-REAL n : ( ( ) ( ) set ) : ( ( V213() ) ( V213() ) L16()) ) equals :: BROUWER:def 2
(TOP-REAL n : ( ( ) ( ) set ) ) : ( ( V213() ) ( V213() ) L16()) | (cl_Ball (x : ( ( ) ( ) set ) ,r : ( ( ) ( ) Element of n : ( ( ) ( ) set ) ) )) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL n : ( ( ) ( ) set ) ) : ( ( V213() ) ( V213() ) L16()) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( strict ) SubSpace of TOP-REAL n : ( ( ) ( ) set ) : ( ( V213() ) ( V213() ) L16()) ) ;

end;

registration

cluster Tdisk (x : ( ( ) ( V16() Function-like V50(n : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Element of the carrier of (TOP-REAL n : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) ) ,r : ( ( non negative real ) ( V11() ext-real non negative real ) set ) ) : ( ( ) ( TopSpace-like ) SubSpace of TOP-REAL n : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) -> non empty ;

end;

theorem :: BROUWER:3

registration

cluster Tdisk (x : ( ( ) ( V16() Function-like V50(n : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Element of the carrier of (TOP-REAL n : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) ) ,r : ( ( real ) ( V11() ext-real real ) set ) ) : ( ( ) ( TopSpace-like ) SubSpace of TOP-REAL n : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) -> convex ;

end;

theorem :: BROUWER:4

for n being ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) )
for r being ( ( non negative real ) ( V11() ext-real non negative real ) number )
for s, t, x being ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) st s : ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) <> t : ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) & s : ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) is ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & s : ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) is not ( ( ) ( ) Point of ( ( ) ( ) set ) ) holds
ex e being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st {e : ( ( ) ( ) Point of ( ( ) ( ) set ) ) } : ( ( ) ( non empty trivial ) set ) = (halfline (s : ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( non empty convex ) Element of bool the carrier of (TOP-REAL b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) /\ (Sphere (x : ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( closed V217( TOP-REAL b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) ) Element of bool the carrier of (TOP-REAL b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BROUWER:5

for n being ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) )
for r being ( ( non negative real ) ( V11() ext-real non negative real ) number )
for s, t, x being ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) st s : ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) <> t : ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) & s : ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) in the carrier of (Tcircle (x : ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( TopSpace-like ) SubSpace of TOP-REAL b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( ) set ) & t : ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) is ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
ex e being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st
( e : ( ( ) ( ) Point of ( ( ) ( ) set ) ) <> s : ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) & {s : ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,e : ( ( ) ( ) Point of ( ( ) ( ) set ) ) } : ( ( ) ( non empty ) set ) = (halfline (s : ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( non empty convex ) Element of bool the carrier of (TOP-REAL b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) /\ (Sphere (x : ( ( ) ( V16() Function-like V50(b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( closed V217( TOP-REAL b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) ) Element of bool the carrier of (TOP-REAL b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL b₁ : ( ( ) ( ordinal natural V11() ext-real non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

definition

func HC (s,t,o,r) -> ( ( ) ( V16() Function-like V50(n : ( ( ) ( ) set ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( ) set ) ) means :: BROUWER:def 3
( it : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of s : ( ( real ) ( V11() ext-real real ) set ) : ( ( ) ( ) set ) ) V20( the carrier of t : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) Function-like total quasi_total ) Element of bool [: the carrier of s : ( ( real ) ( V11() ext-real real ) set ) : ( ( ) ( ) set ) , the carrier of t : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( V16() ) set ) : ( ( ) ( non empty ) set ) ) in (halfline (s : ( ( real ) ( V11() ext-real real ) set ) ,t : ( ( ) ( ) set ) )) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL n : ( ( ) ( ) set ) ) : ( ( V213() ) ( V213() ) L16()) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ (Sphere (o : ( ( ) ( ) set ) ,r : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of n : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) V20( the carrier of o : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) Function-like total quasi_total ) Element of bool [: the carrier of n : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of o : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( V16() ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL n : ( ( ) ( ) set ) ) : ( ( V213() ) ( V213() ) L16()) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL n : ( ( ) ( ) set ) ) : ( ( V213() ) ( V213() ) L16()) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & it : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of s : ( ( real ) ( V11() ext-real real ) set ) : ( ( ) ( ) set ) ) V20( the carrier of t : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) Function-like total quasi_total ) Element of bool [: the carrier of s : ( ( real ) ( V11() ext-real real ) set ) : ( ( ) ( ) set ) , the carrier of t : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( V16() ) set ) : ( ( ) ( non empty ) set ) ) <> s : ( ( real ) ( V11() ext-real real ) set ) );

end;

theorem :: BROUWER:6

theorem :: BROUWER:7

for a being ( ( real ) ( V11() ext-real real ) number )
for r being ( ( non negative real ) ( V11() ext-real non negative real ) number )
for n being ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) )
for s, t, o being ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) )
for S, T, O being ( ( ) ( V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) Element of REAL n : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V53() ) M12( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) )) ) st S : ( ( ) ( V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) Element of REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V53() ) M12( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) )) ) = s : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) & T : ( ( ) ( V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) Element of REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V53() ) M12( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) )) ) = t : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) & O : ( ( ) ( V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) Element of REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V53() ) M12( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) )) ) = o : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) & s : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) is ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & t : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) is ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & s : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) <> t : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) & a : ( ( real ) ( V11() ext-real real ) number ) = ((- |((t : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) - s : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Element of the carrier of (TOP-REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) ) ,(s : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) - o : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Element of the carrier of (TOP-REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) ) )| : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) + (sqrt ((|((t : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) - s : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Element of the carrier of (TOP-REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) ) ,(s : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) - o : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Element of the carrier of (TOP-REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) ) )| : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) ^2) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) - ((Sum (sqr (T : ( ( ) ( V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) Element of REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V53() ) M12( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) )) ) - S : ( ( ) ( V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) Element of REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V53() ) M12( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) )) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) V20( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) M13( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) , REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V53() ) M12( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) )) )) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) V20( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) Function-like V51() complex-yielding V131() V132() ) M13( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ,K373(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ,REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) : ( ( ) ( V53() ) M12( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) )) )) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) * ((Sum (sqr (S : ( ( ) ( V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) Element of REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V53() ) M12( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) )) ) - O : ( ( ) ( V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) Element of REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V53() ) M12( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) )) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) V20( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) M13( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) , REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V53() ) M12( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) )) )) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) V20( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) Function-like V51() complex-yielding V131() V132() ) M13( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ,K373(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ,REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) : ( ( ) ( V53() ) M12( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) )) )) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) - (r : ( ( non negative real ) ( V11() ext-real non negative real ) number ) ^2) : ( ( ) ( V11() ext-real real ) set ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) / (Sum (sqr (T : ( ( ) ( V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) Element of REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V53() ) M12( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) )) ) - S : ( ( ) ( V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) Element of REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V53() ) M12( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) )) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) V20( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) M13( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) , REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V53() ) M12( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) )) )) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) V20( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) Function-like V51() complex-yielding V131() V132() ) M13( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ,K373(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ,REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) : ( ( ) ( V53() ) M12( REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) )) )) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) holds
HC (s : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,o : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( non negative real ) ( V11() ext-real non negative real ) number ) ) : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) = ((1 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) - a : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) * s : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Element of the carrier of (TOP-REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) ) + (a : ( ( real ) ( V11() ext-real real ) number ) * t : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Element of the carrier of (TOP-REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V16() Function-like V50(b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Element of the carrier of (TOP-REAL b₃ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) ) ;

theorem :: BROUWER:8

for a being ( ( real ) ( V11() ext-real real ) number )
for r being ( ( non negative real ) ( V11() ext-real non negative real ) number )
for r1, r2, s1, s2 being ( ( real ) ( V11() ext-real real ) number )
for s, t, o being ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) st s : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) is ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & t : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) is ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & s : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) <> t : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) & r1 : ( ( real ) ( V11() ext-real real ) number ) = (t : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) `1) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) - (s : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) `1) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) & r2 : ( ( real ) ( V11() ext-real real ) number ) = (t : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) - (s : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) & s1 : ( ( real ) ( V11() ext-real real ) number ) = (s : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) `1) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) - (o : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) `1) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) & s2 : ( ( real ) ( V11() ext-real real ) number ) = (s : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) - (o : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) & a : ( ( real ) ( V11() ext-real real ) number ) = ((- ((s1 : ( ( real ) ( V11() ext-real real ) number ) * r1 : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( V11() ext-real real ) set ) + (s2 : ( ( real ) ( V11() ext-real real ) number ) * r2 : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( V11() ext-real real ) set ) ) : ( ( ) ( V11() ext-real real ) set ) ) : ( ( V11() ) ( V11() ext-real real ) set ) + (sqrt ((((s1 : ( ( real ) ( V11() ext-real real ) number ) * r1 : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( V11() ext-real real ) set ) + (s2 : ( ( real ) ( V11() ext-real real ) number ) * r2 : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( V11() ext-real real ) set ) ) : ( ( ) ( V11() ext-real real ) set ) ^2) : ( ( ) ( V11() ext-real real ) set ) - (((r1 : ( ( real ) ( V11() ext-real real ) number ) ^2) : ( ( ) ( V11() ext-real real ) set ) + (r2 : ( ( real ) ( V11() ext-real real ) number ) ^2) : ( ( ) ( V11() ext-real real ) set ) ) : ( ( ) ( V11() ext-real real ) set ) * (((s1 : ( ( real ) ( V11() ext-real real ) number ) ^2) : ( ( ) ( V11() ext-real real ) set ) + (s2 : ( ( real ) ( V11() ext-real real ) number ) ^2) : ( ( ) ( V11() ext-real real ) set ) ) : ( ( ) ( V11() ext-real real ) set ) - (r : ( ( non negative real ) ( V11() ext-real non negative real ) number ) ^2) : ( ( ) ( V11() ext-real real ) set ) ) : ( ( ) ( V11() ext-real real ) set ) ) : ( ( ) ( V11() ext-real real ) set ) ) : ( ( ) ( V11() ext-real real ) set ) ) : ( ( real ) ( V11() ext-real real ) set ) ) : ( ( ) ( V11() ext-real real ) set ) / ((r1 : ( ( real ) ( V11() ext-real real ) number ) ^2) : ( ( ) ( V11() ext-real real ) set ) + (r2 : ( ( real ) ( V11() ext-real real ) number ) ^2) : ( ( ) ( V11() ext-real real ) set ) ) : ( ( ) ( V11() ext-real real ) set ) : ( ( ) ( V11() ext-real real ) set ) holds
HC (s : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,t : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,o : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( non negative real ) ( V11() ext-real non negative real ) number ) ) : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) = |[((s : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) `1) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) + (a : ( ( real ) ( V11() ext-real real ) number ) * r1 : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( V11() ext-real real ) set ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) ,((s : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) + (a : ( ( real ) ( V11() ext-real real ) number ) * r2 : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( V11() ext-real real ) set ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) ) ]| : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) ) ;

definition

let n be ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
let o be ( ( ) ( V16() Function-like V50(n : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ;
let r be ( ( non negative real ) ( V11() ext-real non negative real ) number ) ;
let x be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
let f be ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Tdisk (o : ( ( ) ( V16() Function-like V50(n : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (Tdisk (o : ( ( ) ( V16() Function-like V50(n : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
assume not x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_a_fixpoint_of f : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Tdisk (o : ( ( ) ( V16() Function-like V50(n : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (Tdisk (o : ( ( ) ( V16() Function-like V50(n : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;

func HC (x,f) -> ( ( ) ( ) Point of ( ( ) ( ) set ) ) means :: BROUWER:def 4
ex y, z being ( ( ) ( V16() Function-like V50(n : ( ( ) ( ) set ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( ) set ) ) st
( y : ( ( ) ( V16() Function-like V50(n : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) set ) & z : ( ( ) ( V16() Function-like V50(n : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of n : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) V20( the carrier of o : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) Function-like total quasi_total ) Element of bool [: the carrier of n : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of o : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( V16() ) set ) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of (Tdisk (o : ( ( ) ( ) set ) ,r : ( ( real ) ( V11() ext-real real ) set ) )) : ( ( ) ( TopSpace-like ) SubSpace of TOP-REAL n : ( ( ) ( ) set ) : ( ( V213() ) ( V213() ) L16()) ) : ( ( ) ( ) set ) ) & it : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of r : ( ( real ) ( V11() ext-real real ) set ) : ( ( ) ( ) set ) ) V20( the carrier of x : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) Function-like total quasi_total ) Element of bool [: the carrier of r : ( ( real ) ( V11() ext-real real ) set ) : ( ( ) ( ) set ) , the carrier of x : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( V16() ) set ) : ( ( ) ( non empty ) set ) ) = HC (z : ( ( ) ( V16() Function-like V50(n : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( V16() Function-like V50(n : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,o : ( ( ) ( ) set ) ,r : ( ( real ) ( V11() ext-real real ) set ) ) : ( ( ) ( V16() Function-like V50(n : ( ( ) ( ) set ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( ) set ) ) );

end;

theorem :: BROUWER:9

theorem :: BROUWER:10

definition

func BR-map f -> ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Tdisk (o : ( ( real ) ( V11() ext-real real ) set ) ,r : ( ( ) ( ) set ) )) : ( ( ) ( TopSpace-like ) SubSpace of TOP-REAL n : ( ( ) ( ) set ) : ( ( V213() ) ( V213() ) L16()) ) : ( ( ) ( ) set ) ) V20( the carrier of (Tcircle (o : ( ( real ) ( V11() ext-real real ) set ) ,r : ( ( ) ( ) set ) )) : ( ( ) ( TopSpace-like ) SubSpace of TOP-REAL n : ( ( ) ( ) set ) : ( ( V213() ) ( V213() ) L16()) ) : ( ( ) ( ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) means :: BROUWER:def 5
for x being ( ( ) ( ) Point of ( ( ) ( ) set ) ) holds it : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of n : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) V20( the carrier of r : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) Function-like total quasi_total ) Element of bool [: the carrier of n : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of r : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( V16() ) set ) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (Tcircle (o : ( ( real ) ( V11() ext-real real ) set ) ,r : ( ( ) ( ) set ) )) : ( ( ) ( TopSpace-like ) SubSpace of TOP-REAL n : ( ( ) ( ) set ) : ( ( V213() ) ( V213() ) L16()) ) : ( ( ) ( ) set ) ) = HC (x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,f : ( ( ) ( ) set ) ) : ( ( ) ( ) Point of ( ( ) ( ) set ) ) ;

end;

theorem :: BROUWER:11

theorem :: BROUWER:12

for r being ( ( non negative real ) ( V11() ext-real non negative real ) number )
for n being ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) )
for o being ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of (Tdisk (b₃ : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (Tdisk (b₃ : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of (Tdisk (b₃ : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (Tdisk (b₃ : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is without_fixpoints holds
(BR-map f : ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of (Tdisk (b₃ : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (Tdisk (b₃ : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Tdisk (b₃ : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (Tcircle (b₃ : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) | (Sphere (o : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty closed V217( TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) ) Element of bool the carrier of (TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( V16() V19( Sphere (b₃ : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) ) : ( ( ) ( non empty closed V217( TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) ) Element of bool the carrier of (TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V19( the carrier of (Tdisk (b₃ : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (Tcircle (b₃ : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) Function-like ) Element of bool [: the carrier of (Tdisk (b₃ : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) , the carrier of (Tcircle (b₃ : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty V16() ) set ) : ( ( ) ( non empty ) set ) ) = id (Tcircle (o : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Tcircle (b₃ : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (Tcircle (b₃ : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of bool [: the carrier of (Tcircle (b₃ : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) , the carrier of (Tcircle (b₃ : ( ( ) ( V16() Function-like V50(b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL b₂ : ( ( non empty ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty V16() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BROUWER:13

for r being ( ( positive real ) ( non empty V11() ext-real positive non negative real ) number )
for o being ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of (Tdisk (b₂ : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( positive real ) ( non empty V11() ext-real positive non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (Tdisk (b₂ : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( positive real ) ( non empty V11() ext-real positive non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of (Tdisk (b₂ : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( positive real ) ( non empty V11() ext-real positive non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (Tdisk (b₂ : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( positive real ) ( non empty V11() ext-real positive non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is without_fixpoints holds
BR-map f : ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of (Tdisk (b₂ : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( positive real ) ( non empty V11() ext-real positive non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (Tdisk (b₂ : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( positive real ) ( non empty V11() ext-real positive non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (Tdisk (b₂ : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( positive real ) ( non empty V11() ext-real positive non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (Tcircle (b₂ : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( positive real ) ( non empty V11() ext-real positive non negative real ) number ) )) : ( ( ) ( non empty strict TopSpace-like pathwise_connected V236() ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous ;

theorem :: BROUWER:14

for r being ( ( non negative real ) ( V11() ext-real non negative real ) number )
for o being ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of (Tdisk (b₂ : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (Tdisk (b₂ : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds f : ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of (Tdisk (b₂ : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (Tdisk (b₂ : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is with_fixpoint ;

theorem :: BROUWER:15

for r being ( ( non negative real ) ( V11() ext-real non negative real ) number )
for o being ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of (Tdisk (b₂ : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (Tdisk (b₂ : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ex x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of (Tdisk (b₂ : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (Tdisk (b₂ : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (Tdisk (b₂ : ( ( ) ( V16() Function-like V50(2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) ) V51() complex-yielding V131() V132() ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() ext-real positive non negative real V33() V34() V140() V141() V142() V143() V144() V145() ) Element of NAT : ( ( ) ( V140() V141() V142() V143() V144() V145() V146() ) Element of bool REAL : ( ( ) ( non empty V43() V140() V141() V142() V146() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( V213() ) ( non empty V87() V152() V153() TopSpace-like V201() V202() V203() V204() V205() V206() V207() V213() ) L16()) ) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;