URYSOHN1

:: URYSOHN1 semantic presentation

definition

let n be ( ( V26() ) ( V26() V27() V28() ext-real ) Nat) ;

func dyadic n -> ( ( ) ( V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) means :: URYSOHN1:def 1
for x being ( ( ) ( V27() V28() ext-real ) Real) holds
( x : ( ( ) ( V27() V28() ext-real ) Real) in it : ( ( ) ( ) Element of bool (bool n : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) iff ex i being ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) st
( i : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) <= 2 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) |^ n : ( ( ) ( ) TopStruct ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) & x : ( ( ) ( V27() V28() ext-real ) Real) = i : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) / (2 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) |^ n : ( ( ) ( ) TopStruct ) ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) ) );

end;

definition

func DYADIC -> ( ( ) ( V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) means :: URYSOHN1:def 2
for a being ( ( ) ( V27() V28() ext-real ) Real) holds
( a : ( ( ) ( V27() V28() ext-real ) Real) in it : ( ( ) ( ) TopStruct ) iff ex n being ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) st a : ( ( ) ( V27() V28() ext-real ) Real) in dyadic n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) );

end;

definition

func DOM -> ( ( ) ( V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) equals :: URYSOHN1:def 3
((halfline 0 : ( ( ) ( empty V26() V27() V28() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V36() V37() V38() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) \/ DYADIC : ( ( ) ( V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V36() V37() V38() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) \/ (right_open_halfline 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V36() V37() V38() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V36() V37() V38() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

definition

let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
let A be ( ( non empty ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ;
let F be ( ( Function-like V33(A : ( ( non empty ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13(A : ( ( non empty ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33(A : ( ( non empty ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) Function of A : ( ( non empty ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
let r be ( ( ) ( V27() V28() ext-real ) Element of A : ( ( non empty ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) ;
:: original: .
redefine func F . r -> ( ( ) ( ) Subset of ) ;

end;

theorem :: URYSOHN1:1

theorem :: URYSOHN1:2

dyadic 0 : ( ( ) ( empty V26() V27() V28() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) = {0 : ( ( ) ( empty V26() V27() V28() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: URYSOHN1:3

dyadic 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) = {0 : ( ( ) ( empty V26() V27() V28() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ,(1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V27() V28() ext-real non negative ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) ,1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty V36() V37() V38() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ;

registration

let n be ( ( V26() ) ( V26() V27() V28() ext-real ) Nat) ;

cluster dyadic n : ( ( V26() ) ( V26() V27() V28() ext-real ) set ) : ( ( ) ( V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) -> non empty ;

end;

definition

let n be ( ( V26() ) ( V26() V27() V28() ext-real ) Nat) ;

func dyad n -> ( ( V10() Function-like FinSequence-like ) ( V10() Function-like FinSequence-like ) FinSequence) means :: URYSOHN1:def 4
( dom it : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( V36() V37() V38() V39() V40() V41() ) Element of bool NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = Seg ((2 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) |^ n : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V36() V37() V38() V39() V40() V41() ) Element of bool NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & ( for i being ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) st i : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) in dom it : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( V36() V37() V38() V39() V40() V41() ) Element of bool NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
it : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) . i : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = (i : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) - 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) / (2 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) |^ n : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) ) );

end;

theorem :: URYSOHN1:4

registration

cluster DYADIC : ( ( ) ( V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) -> non empty ;

end;

registration

cluster DOM : ( ( ) ( V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) -> non empty ;

end;

theorem :: URYSOHN1:5

theorem :: URYSOHN1:6

theorem :: URYSOHN1:7

for n, i being ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) st 0 : ( ( ) ( empty V26() V27() V28() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) < i : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) & i : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) <= 2 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) |^ n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
((i : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) * 2 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) - 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) / (2 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) |^ (n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) in (dyadic (n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) \ (dyadic n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V36() V37() V38() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: URYSOHN1:8

for n, i being ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) st 0 : ( ( ) ( empty V26() V27() V28() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) <= i : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) & i : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) < 2 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) |^ n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
((i : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) * 2 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) / (2 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) |^ (n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) in (dyadic (n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) \ (dyadic n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V36() V37() V38() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: URYSOHN1:9

definition

let n be ( ( V26() ) ( V26() V27() V28() ext-real ) Nat) ;
let x be ( ( ) ( V27() V28() ext-real ) Element of dyadic n : ( ( V26() ) ( V26() V27() V28() ext-real ) Nat) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) ;

func axis x -> ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) means :: URYSOHN1:def 5
x : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) = it : ( ( ) ( ) Element of n : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) / (2 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) |^ n : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) ;

end;

theorem :: URYSOHN1:10

theorem :: URYSOHN1:11

theorem :: URYSOHN1:12

theorem :: URYSOHN1:13

for n being ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) )
for x being ( ( ) ( V27() V28() ext-real ) Element of dyadic (n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) st not x : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₁ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) in dyadic n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) holds
( ((axis x : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₁ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) - 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) / (2 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) |^ (n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) in dyadic n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) & ((axis x : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₁ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) / (2 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) |^ (n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) in dyadic n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: URYSOHN1:14

theorem :: URYSOHN1:15

theorem :: URYSOHN1:16

for n being ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) )
for x1, x2 being ( ( ) ( V27() V28() ext-real ) Element of dyadic (n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) st x1 : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₁ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) < x2 : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₁ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) & not x1 : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₁ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) in dyadic n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) & not x2 : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₁ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) in dyadic n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) holds
((axis x1 : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₁ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) / (2 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) |^ (n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) <= ((axis x2 : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₁ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) - 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) / (2 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) |^ (n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V27() V28() ext-real ) Element of REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) ) ;

notation

let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let x be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
synonym Nbhd of x,T for a_neighborhood of x;

end;

definition

let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let x be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;

redefine mode a_neighborhood of x means :: URYSOHN1:def 6
ex A being ( ( ) ( ) Subset of ) st
( A : ( ( ) ( ) Subset of ) is open & x : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) in A : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) c= it : ( ( ) ( ) Element of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) );

end;

theorem :: URYSOHN1:17

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) holds
( A : ( ( ) ( ) Subset of ) is open iff for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) holds
ex B being ( ( ) ( ) Nbhd of x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) st B : ( ( ) ( ) Nbhd of b₃ : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) c= A : ( ( ) ( ) Subset of ) ) ;

theorem :: URYSOHN1:18

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) st ( for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) holds
A : ( ( ) ( ) Subset of ) is ( ( ) ( ) Nbhd of x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) holds
A : ( ( ) ( ) Subset of ) is open ;

definition

let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;

redefine attr T is T_1 means :: URYSOHN1:def 7
for p, q being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st not p : ( ( ) ( ) Point of ( ( ) ( ) set ) ) = q : ( ( ) ( ) Point of ( ( ) ( ) set ) ) holds
ex W, V being ( ( ) ( ) Subset of ) st
( W : ( ( ) ( ) Subset of ) is open & V : ( ( ) ( ) Subset of ) is open & p : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in W : ( ( ) ( ) Subset of ) & not q : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in W : ( ( ) ( ) Subset of ) & q : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in V : ( ( ) ( ) Subset of ) & not p : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in V : ( ( ) ( ) Subset of ) );

end;

theorem :: URYSOHN1:19

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is T_1 iff for p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds {p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is closed ) ;

theorem :: URYSOHN1:20

theorem :: URYSOHN1:21

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is regular iff for A being ( ( open ) ( open ) Subset of )
for p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in A : ( ( open ) ( open ) Subset of ) holds
ex B being ( ( open ) ( open ) Subset of ) st
( p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in B : ( ( open ) ( open ) Subset of ) & Cl B : ( ( open ) ( open ) Subset of ) : ( ( ) ( closed ) Element of bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= A : ( ( open ) ( open ) Subset of ) ) ) ;

theorem :: URYSOHN1:22

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is normal & T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is T_1 holds
for A being ( ( open ) ( open ) Subset of ) st A : ( ( open ) ( open ) Subset of ) <> {} : ( ( ) ( empty V36() V37() V38() V39() V40() V41() V42() ) set ) holds
ex B being ( ( ) ( ) Subset of ) st
( B : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( empty V36() V37() V38() V39() V40() V41() V42() ) set ) & Cl B : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= A : ( ( open ) ( open ) Subset of ) ) ;

theorem :: URYSOHN1:23

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is normal holds
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is open & B : ( ( ) ( ) Subset of ) is closed & B : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( empty V36() V37() V38() V39() V40() V41() V42() ) set ) & B : ( ( ) ( ) Subset of ) c= A : ( ( ) ( ) Subset of ) holds
ex C being ( ( ) ( ) Subset of ) st
( C : ( ( ) ( ) Subset of ) is open & B : ( ( ) ( ) Subset of ) c= C : ( ( ) ( ) Subset of ) & Cl C : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ) ) ;

definition

let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let A, B be ( ( ) ( ) Subset of ) ;
assume ( T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is normal & A : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( empty V36() V37() V38() V39() V40() V41() V42() ) set ) & A : ( ( ) ( ) Subset of ) is open & B : ( ( ) ( ) Subset of ) is open & Cl A : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ) ) ;

mode Between of A,B -> ( ( ) ( ) Subset of ) means :: URYSOHN1:def 8
( it : ( ( ) ( ) set ) <> {} : ( ( ) ( empty V36() V37() V38() V39() V40() V41() V42() ) set ) & it : ( ( ) ( ) set ) is open & Cl A : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= it : ( ( ) ( ) set ) & Cl it : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Element of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) );

end;

theorem :: URYSOHN1:24

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is normal holds
for A, B being ( ( closed ) ( closed ) Subset of ) st A : ( ( closed ) ( closed ) Subset of ) <> {} : ( ( ) ( empty V36() V37() V38() V39() V40() V41() V42() ) set ) holds
for n being ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) )
for G being ( ( Function-like V33( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) st A : ( ( closed ) ( closed ) Subset of ) c= G : ( ( Function-like V33( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . 0 : ( ( ) ( empty V26() V27() V28() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) & B : ( ( closed ) ( closed ) Subset of ) = ([#] T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty non proper open closed dense non boundary ) Element of bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) \ (G : ( ( Function-like V33( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & ( for r1, r2 being ( ( ) ( V27() V28() ext-real ) Element of dyadic n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) st r1 : ( ( Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) < r2 : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) holds
( G : ( ( Function-like V33( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . r1 : ( ( Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) is open & G : ( ( Function-like V33( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . r2 : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) is open & Cl (G : ( ( Function-like V33( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . r1 : ( ( Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= G : ( ( Function-like V33( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . r2 : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) ) ) holds
ex F being ( ( Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic (n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) st
( A : ( ( closed ) ( closed ) Subset of ) c= F : ( ( Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . 0 : ( ( ) ( empty V26() V27() V28() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) & B : ( ( closed ) ( closed ) Subset of ) = ([#] T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty non proper open closed dense non boundary ) Element of bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) \ (F : ( ( Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & ( for r1, r2, r being ( ( ) ( V27() V28() ext-real ) Element of dyadic (n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) st r1 : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) < r2 : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) holds
( F : ( ( Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . r1 : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) is open & F : ( ( Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . r2 : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) is open & Cl (F : ( ( Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . r1 : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= F : ( ( Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . r2 : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) & ( r : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) in dyadic n : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) implies F : ( ( Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . r : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) = G : ( ( Function-like V33( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ( V10() V13( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) V14( bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) Function-like V33( dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function of dyadic b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) , bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . r : ( ( ) ( V27() V28() ext-real ) Element of dyadic (b₄ : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() ) Element of NAT : ( ( ) ( V36() V37() V38() V39() V40() V41() V42() ) Element of bool REAL : ( ( ) ( non empty V36() V37() V38() V42() V43() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V36() V37() V38() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) ) ) ) ;