:: TOPREALA semantic presentation

begin

registration
let r be ( ( real ) ( V28() real ext-real ) number ) ;
let s be ( ( real positive ) ( non empty V28() real ext-real positive non negative ) number ) ;
cluster K148(r : ( ( real ) ( V28() real ext-real ) set ) ,(r : ( ( real ) ( V28() real ext-real ) set ) + s : ( ( real positive ) ( non empty V28() real ext-real positive non negative ) set ) ) : ( ( ) ( V28() real ext-real ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster K146(r : ( ( real ) ( V28() real ext-real ) set ) ,(r : ( ( real ) ( V28() real ext-real ) set ) + s : ( ( real positive ) ( non empty V28() real ext-real positive non negative ) set ) ) : ( ( ) ( V28() real ext-real ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster K147(r : ( ( real ) ( V28() real ext-real ) set ) ,(r : ( ( real ) ( V28() real ext-real ) set ) + s : ( ( real positive ) ( non empty V28() real ext-real positive non negative ) set ) ) : ( ( ) ( V28() real ext-real ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster K145(r : ( ( real ) ( V28() real ext-real ) set ) ,(r : ( ( real ) ( V28() real ext-real ) set ) + s : ( ( real positive ) ( non empty V28() real ext-real positive non negative ) set ) ) : ( ( ) ( V28() real ext-real ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster K148((r : ( ( real ) ( V28() real ext-real ) set ) - s : ( ( real positive ) ( non empty V28() real ext-real positive non negative ) set ) ) : ( ( ) ( V28() real ext-real ) set ) ,r : ( ( real ) ( V28() real ext-real ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster K146((r : ( ( real ) ( V28() real ext-real ) set ) - s : ( ( real positive ) ( non empty V28() real ext-real positive non negative ) set ) ) : ( ( ) ( V28() real ext-real ) set ) ,r : ( ( real ) ( V28() real ext-real ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster K147((r : ( ( real ) ( V28() real ext-real ) set ) - s : ( ( real positive ) ( non empty V28() real ext-real positive non negative ) set ) ) : ( ( ) ( V28() real ext-real ) set ) ,r : ( ( real ) ( V28() real ext-real ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster K145((r : ( ( real ) ( V28() real ext-real ) set ) - s : ( ( real positive ) ( non empty V28() real ext-real positive non negative ) set ) ) : ( ( ) ( V28() real ext-real ) set ) ,r : ( ( real ) ( V28() real ext-real ) set ) ) : ( ( ) ( ) set ) -> non empty ;
end;

registration
let r be ( ( real non positive ) ( V28() real ext-real non positive ) number ) ;
let s be ( ( real positive ) ( non empty V28() real ext-real positive non negative ) number ) ;
cluster K148(r : ( ( real non positive ) ( V28() real ext-real non positive ) set ) ,s : ( ( real positive ) ( non empty V28() real ext-real positive non negative ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster K146(r : ( ( real non positive ) ( V28() real ext-real non positive ) set ) ,s : ( ( real positive ) ( non empty V28() real ext-real positive non negative ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster K147(r : ( ( real non positive ) ( V28() real ext-real non positive ) set ) ,s : ( ( real positive ) ( non empty V28() real ext-real positive non negative ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster K145(r : ( ( real non positive ) ( V28() real ext-real non positive ) set ) ,s : ( ( real positive ) ( non empty V28() real ext-real positive non negative ) set ) ) : ( ( ) ( ) set ) -> non empty ;
end;

registration
let r be ( ( real negative ) ( non empty V28() real ext-real non positive negative ) number ) ;
let s be ( ( real non negative ) ( V28() real ext-real non negative ) number ) ;
cluster K148(r : ( ( real negative ) ( non empty V28() real ext-real non positive negative ) set ) ,s : ( ( real non negative ) ( V28() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster K146(r : ( ( real negative ) ( non empty V28() real ext-real non positive negative ) set ) ,s : ( ( real non negative ) ( V28() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster K147(r : ( ( real negative ) ( non empty V28() real ext-real non positive negative ) set ) ,s : ( ( real non negative ) ( V28() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster K145(r : ( ( real negative ) ( non empty V28() real ext-real non positive negative ) set ) ,s : ( ( real non negative ) ( V28() real ext-real non negative ) set ) ) : ( ( ) ( ) set ) -> non empty ;
end;

begin

theorem :: TOPREALA:1
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for x, X being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) in f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) .: X : ( ( ) ( ) set ) : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is one-to-one holds
x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) ;

theorem :: TOPREALA:2
for f being ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) -defined Function-like V30() FinSequence-like FinSubsequence-like ) FinSequence)
for i being ( ( natural ) ( natural V28() real ext-real ) Nat) holds
( not i : ( ( natural ) ( natural V28() real ext-real ) Nat) + 1 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) in dom f : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) -defined Function-like V30() FinSequence-like FinSubsequence-like ) FinSequence) : ( ( ) ( V176() V177() V178() V179() V180() V181() ) Element of bool NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) or i : ( ( natural ) ( natural V28() real ext-real ) Nat) in dom f : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) -defined Function-like V30() FinSequence-like FinSubsequence-like ) FinSequence) : ( ( ) ( V176() V177() V178() V179() V180() V181() ) Element of bool NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) or i : ( ( natural ) ( natural V28() real ext-real ) Nat) = 0 : ( ( ) ( natural V28() real ext-real integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: TOPREALA:3
for x, y, X, Y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st x : ( ( ) ( ) set ) <> y : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in product ((x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ) --> (X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) )) : ( ( ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) holds
( f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . y : ( ( ) ( ) set ) : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) ) ;

theorem :: TOPREALA:4
for a, b being ( ( ) ( ) set ) holds <*a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) -defined Function-like non empty V30() V37(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) set ) = (1 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) --> (a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined Function-like ) set ) ;

begin

registration
cluster non empty strict TopSpace-like constituted-FinSeqs for ( ( ) ( ) TopStruct ) ;
end;

registration
let T be ( ( TopSpace-like constituted-FinSeqs ) ( TopSpace-like constituted-Functions constituted-FinSeqs ) TopSpace) ;
cluster -> constituted-FinSeqs for ( ( ) ( ) SubSpace of T : ( ( ) ( ) set ) ) ;
end;

theorem :: TOPREALA:5
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for Z being ( ( non empty ) ( non empty TopSpace-like ) SubSpace of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )
for t being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for z being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for N being ( ( open ) ( non empty open ) a_neighborhood of t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )
for M being ( ( ) ( ) Subset of ) st t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = z : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & M : ( ( ) ( ) Subset of ) = N : ( ( open ) ( non empty open ) a_neighborhood of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) /\ ([#] Z : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) : ( ( ) ( non empty non proper open closed dense non boundary ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) holds
M : ( ( ) ( ) Subset of ) is ( ( open ) ( non empty open ) a_neighborhood of z : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ;

registration
cluster empty TopSpace-like -> TopSpace-like discrete anti-discrete for ( ( ) ( ) TopStruct ) ;
end;

registration
let X be ( ( TopSpace-like discrete ) ( TopSpace-like discrete ) TopSpace) ;
let Y be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
cluster Function-like quasi_total -> Function-like quasi_total continuous for ( ( ) ( ) Element of bool [: the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: TOPREALA:6
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for Y being ( ( ) ( ) TopStruct )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is empty holds
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is continuous ;

registration
let X be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
let Y be ( ( ) ( ) TopStruct ) ;
cluster Function-like empty quasi_total -> Function-like quasi_total continuous for ( ( ) ( ) Element of bool [: the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: TOPREALA:7
for X being ( ( ) ( ) TopStruct )
for Y being ( ( non empty ) ( non empty ) TopStruct )
for Z being ( ( non empty ) ( non empty ) SubSpace of Y : ( ( non empty ) ( non empty ) TopStruct ) )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) SubSpace of b2 : ( ( non empty ) ( non empty ) TopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) holds f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) SubSpace of b2 : ( ( non empty ) ( non empty ) TopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) is ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) ;

theorem :: TOPREALA:8
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for X being ( ( ) ( ) Subset of )
for Y being ( ( ) ( ) Subset of )
for f being ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( Relation-like the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st g : ( ( Function-like quasi_total ) ( Relation-like the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) = f : ( ( Function-like quasi_total continuous ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) | X : ( ( ) ( ) Subset of ) : ( ( Function-like ) ( Relation-like b3 : ( ( ) ( ) Subset of ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) holds
g : ( ( Function-like quasi_total ) ( Relation-like the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is continuous ;

theorem :: TOPREALA:9
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for Z being ( ( non empty ) ( non empty TopSpace-like ) SubSpace of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is open holds
g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is open ;

theorem :: TOPREALA:10
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for S1 being ( ( ) ( ) Subset of )
for T1 being ( ( ) ( ) Subset of )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( Relation-like the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st g : ( ( Function-like quasi_total ) ( Relation-like the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) = f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) | S1 : ( ( ) ( ) Subset of ) : ( ( Function-like ) ( Relation-like b3 : ( ( ) ( ) Subset of ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is onto & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is open & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is one-to-one holds
g : ( ( Function-like quasi_total ) ( Relation-like the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -defined the carrier of (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is open ;

theorem :: TOPREALA:11
for X, Y, Z being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is open & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is open holds
g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is open ;

theorem :: TOPREALA:12
for X, Y being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for Z being ( ( open ) ( TopSpace-like open ) SubSpace of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) )
for g being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( open ) ( TopSpace-like open ) SubSpace of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) = g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( open ) ( TopSpace-like open ) SubSpace of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b3 : ( ( open ) ( TopSpace-like open ) SubSpace of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is open holds
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is open ;

theorem :: TOPREALA:13
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is one-to-one & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is onto holds
( f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous iff f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of bool [: the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is open ) ;

theorem :: TOPREALA:14
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is one-to-one & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is onto holds
( f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is open iff f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of bool [: the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is continuous ) ;

theorem :: TOPREALA:15
for S being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) are_homeomorphic iff TopStruct(# the carrier of S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) , TopStruct(# the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the topology of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) are_homeomorphic ) ;

theorem :: TOPREALA:16
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is one-to-one & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is onto & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is open holds
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism ;

begin

theorem :: TOPREALA:17
for r being ( ( real ) ( V28() real ext-real ) number )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) = REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) --> r : ( ( real ) ( V28() real ext-real ) number ) : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined {b1 : ( ( real ) ( V28() real ext-real ) number ) } : ( ( ) ( V176() V177() V178() ) set ) -valued Function-like quasi_total V166() V167() V168() ) Element of bool [:REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ,{b1 : ( ( real ) ( V28() real ext-real ) number ) } : ( ( ) ( V176() V177() V178() ) set ) :] : ( ( ) ( Relation-like V166() V167() V168() ) set ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) | REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) Element of bool [:REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ,REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) :] : ( ( ) ( Relation-like V166() V167() V168() ) set ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: TOPREALA:18
for f, f1, f2 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) st dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) = (dom f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) ) : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) \/ (dom f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) ) : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) & dom f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) is open & dom f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) is open & f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) | (dom f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) ) : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined dom b2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) Element of bool [:REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ,REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) :] : ( ( ) ( Relation-like V166() V167() V168() ) set ) : ( ( ) ( ) set ) ) is continuous & f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) | (dom f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) ) : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined dom b3 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) Element of bool [:REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ,REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) :] : ( ( ) ( Relation-like V166() V167() V168() ) set ) : ( ( ) ( ) set ) ) is continuous & ( for z being ( ( ) ( ) set ) st z : ( ( ) ( ) set ) in dom f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) . z : ( ( ) ( ) set ) : ( ( ) ( V28() real ext-real ) set ) = f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) . z : ( ( ) ( ) set ) : ( ( ) ( V28() real ext-real ) set ) ) & ( for z being ( ( ) ( ) set ) st z : ( ( ) ( ) set ) in dom f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) . z : ( ( ) ( ) set ) : ( ( ) ( V28() real ext-real ) set ) = f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) . z : ( ( ) ( ) set ) : ( ( ) ( V28() real ext-real ) set ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) | (dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) ) : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined dom b1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) Element of bool [:REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ,REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) :] : ( ( ) ( Relation-like V166() V167() V168() ) set ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: TOPREALA:19
for x being ( ( ) ( V28() real ext-real ) Point of ( ( ) ( non empty V176() V177() V178() ) set ) )
for N being ( ( ) ( V176() V177() V178() ) Subset of ( ( ) ( ) set ) )
for M being ( ( ) ( V176() V177() V178() ) Subset of ) st M : ( ( ) ( V176() V177() V178() ) Subset of ) = N : ( ( ) ( V176() V177() V178() ) Subset of ( ( ) ( ) set ) ) & N : ( ( ) ( V176() V177() V178() ) Subset of ( ( ) ( ) set ) ) is ( ( ) ( V176() V177() V178() ) Neighbourhood of x : ( ( ) ( V28() real ext-real ) Point of ( ( ) ( non empty V176() V177() V178() ) set ) ) ) holds
M : ( ( ) ( V176() V177() V178() ) Subset of ) is ( ( ) ( non empty V176() V177() V178() ) a_neighborhood of x : ( ( ) ( V28() real ext-real ) Point of ( ( ) ( non empty V176() V177() V178() ) set ) ) ) ;

theorem :: TOPREALA:20
for x being ( ( ) ( V28() real ext-real ) Point of ( ( ) ( non empty V176() V177() V178() ) set ) )
for M being ( ( ) ( non empty V176() V177() V178() ) a_neighborhood of x : ( ( ) ( V28() real ext-real ) Point of ( ( ) ( non empty V176() V177() V178() ) set ) ) ) ex N being ( ( ) ( V176() V177() V178() ) Neighbourhood of x : ( ( ) ( V28() real ext-real ) Point of ( ( ) ( non empty V176() V177() V178() ) set ) ) ) st N : ( ( ) ( V176() V177() V178() ) Neighbourhood of b1 : ( ( ) ( V28() real ext-real ) Point of ( ( ) ( non empty V176() V177() V178() ) set ) ) ) c= M : ( ( ) ( non empty V176() V177() V178() ) a_neighborhood of b1 : ( ( ) ( V28() real ext-real ) Point of ( ( ) ( non empty V176() V177() V178() ) set ) ) ) ;

theorem :: TOPREALA:21
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) : ( ( ) ( non empty V176() V177() V178() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) : ( ( ) ( non empty V176() V177() V178() ) set ) -valued Function-like non empty total quasi_total V166() V167() V168() ) Function of ( ( ) ( non empty V176() V177() V178() ) set ) , ( ( ) ( non empty V176() V177() V178() ) set ) )
for g being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,)
for x being ( ( ) ( V28() real ext-real ) Point of ( ( ) ( non empty V176() V177() V178() ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) : ( ( ) ( non empty V176() V177() V178() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) : ( ( ) ( non empty V176() V177() V178() ) set ) -valued Function-like non empty total quasi_total V166() V167() V168() ) Function of ( ( ) ( non empty V176() V177() V178() ) set ) , ( ( ) ( non empty V176() V177() V178() ) set ) ) = g : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) & g : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like V166() V167() V168() ) PartFunc of ,) is_continuous_in x : ( ( ) ( V28() real ext-real ) Point of ( ( ) ( non empty V176() V177() V178() ) set ) ) holds
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) : ( ( ) ( non empty V176() V177() V178() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) : ( ( ) ( non empty V176() V177() V178() ) set ) -valued Function-like non empty total quasi_total V166() V167() V168() ) Function of ( ( ) ( non empty V176() V177() V178() ) set ) , ( ( ) ( non empty V176() V177() V178() ) set ) ) is_continuous_at x : ( ( ) ( V28() real ext-real ) Point of ( ( ) ( non empty V176() V177() V178() ) set ) ) ;

theorem :: TOPREALA:22
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) : ( ( ) ( non empty V176() V177() V178() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) : ( ( ) ( non empty V176() V177() V178() ) set ) -valued Function-like non empty total quasi_total V166() V167() V168() ) Function of ( ( ) ( non empty V176() V177() V178() ) set ) , ( ( ) ( non empty V176() V177() V178() ) set ) )
for g being ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like non empty total quasi_total V166() V167() V168() ) Function of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) , REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) : ( ( ) ( non empty V176() V177() V178() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) : ( ( ) ( non empty V176() V177() V178() ) set ) -valued Function-like non empty total quasi_total V166() V167() V168() ) Function of ( ( ) ( non empty V176() V177() V178() ) set ) , ( ( ) ( non empty V176() V177() V178() ) set ) ) = g : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like non empty total quasi_total V166() V167() V168() ) Function of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) , REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) & g : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -valued Function-like non empty total quasi_total V166() V167() V168() ) Function of REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) , REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) ) is continuous holds
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) : ( ( ) ( non empty V176() V177() V178() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) : ( ( ) ( non empty V176() V177() V178() ) set ) -valued Function-like non empty total quasi_total V166() V167() V168() ) Function of ( ( ) ( non empty V176() V177() V178() ) set ) , ( ( ) ( non empty V176() V177() V178() ) set ) ) is continuous ;

theorem :: TOPREALA:23
for a, r, s, b being ( ( real ) ( V28() real ext-real ) number ) st a : ( ( real ) ( V28() real ext-real ) number ) <= r : ( ( real ) ( V28() real ext-real ) number ) & s : ( ( real ) ( V28() real ext-real ) number ) <= b : ( ( real ) ( V28() real ext-real ) number ) holds
[.r : ( ( real ) ( V28() real ext-real ) number ) ,s : ( ( real ) ( V28() real ext-real ) number ) .] : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) is ( ( closed ) ( closed V176() V177() V178() ) Subset of ) ;

theorem :: TOPREALA:24
for a, r, s, b being ( ( real ) ( V28() real ext-real ) number ) st a : ( ( real ) ( V28() real ext-real ) number ) <= r : ( ( real ) ( V28() real ext-real ) number ) & s : ( ( real ) ( V28() real ext-real ) number ) <= b : ( ( real ) ( V28() real ext-real ) number ) holds
].r : ( ( real ) ( V28() real ext-real ) number ) ,s : ( ( real ) ( V28() real ext-real ) number ) .[ : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) is ( ( open ) ( open V176() V177() V178() ) Subset of ) ;

theorem :: TOPREALA:25
for a, b, r being ( ( real ) ( V28() real ext-real ) number ) st a : ( ( real ) ( V28() real ext-real ) number ) <= b : ( ( real ) ( V28() real ext-real ) number ) & a : ( ( real ) ( V28() real ext-real ) number ) <= r : ( ( real ) ( V28() real ext-real ) number ) holds
].r : ( ( real ) ( V28() real ext-real ) number ) ,b : ( ( real ) ( V28() real ext-real ) number ) .] : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) is ( ( open ) ( open V176() V177() V178() ) Subset of ) ;

theorem :: TOPREALA:26
for a, b, r being ( ( real ) ( V28() real ext-real ) number ) st a : ( ( real ) ( V28() real ext-real ) number ) <= b : ( ( real ) ( V28() real ext-real ) number ) & r : ( ( real ) ( V28() real ext-real ) number ) <= b : ( ( real ) ( V28() real ext-real ) number ) holds
[.a : ( ( real ) ( V28() real ext-real ) number ) ,r : ( ( real ) ( V28() real ext-real ) number ) .[ : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) is ( ( open ) ( open V176() V177() V178() ) Subset of ) ;

theorem :: TOPREALA:27
for a, b, r, s being ( ( real ) ( V28() real ext-real ) number ) st a : ( ( real ) ( V28() real ext-real ) number ) <= b : ( ( real ) ( V28() real ext-real ) number ) & r : ( ( real ) ( V28() real ext-real ) number ) <= s : ( ( real ) ( V28() real ext-real ) number ) holds
the carrier of [:(Closed-Interval-TSpace (a : ( ( real ) ( V28() real ext-real ) number ) ,b : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) ,(Closed-Interval-TSpace (r : ( ( real ) ( V28() real ext-real ) number ) ,s : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) = [:[.a : ( ( real ) ( V28() real ext-real ) number ) ,b : ( ( real ) ( V28() real ext-real ) number ) .] : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ,[.r : ( ( real ) ( V28() real ext-real ) number ) ,s : ( ( real ) ( V28() real ext-real ) number ) .] : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like V166() V167() V168() ) set ) ;

begin

theorem :: TOPREALA:28
for a, b being ( ( real ) ( V28() real ext-real ) number ) holds |[a : ( ( real ) ( V28() real ext-real ) number ) ,b : ( ( real ) ( V28() real ext-real ) number ) ]| : ( ( ) ( Relation-like NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) -defined Function-like non empty V30() V37(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V166() V167() V168() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) : ( ( ) ( non empty ) set ) ) = (1 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) --> (a : ( ( real ) ( V28() real ext-real ) number ) ,b : ( ( real ) ( V28() real ext-real ) number ) ) : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined Function-like ) set ) ;

theorem :: TOPREALA:29
for a, b being ( ( real ) ( V28() real ext-real ) number ) holds
( |[a : ( ( real ) ( V28() real ext-real ) number ) ,b : ( ( real ) ( V28() real ext-real ) number ) ]| : ( ( ) ( Relation-like NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) -defined Function-like non empty V30() V37(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V166() V167() V168() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) : ( ( ) ( non empty ) set ) ) . 1 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V28() real ext-real ) set ) = a : ( ( real ) ( V28() real ext-real ) number ) & |[a : ( ( real ) ( V28() real ext-real ) number ) ,b : ( ( real ) ( V28() real ext-real ) number ) ]| : ( ( ) ( Relation-like NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) -defined Function-like non empty V30() V37(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V166() V167() V168() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) : ( ( ) ( non empty ) set ) ) . 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V28() real ext-real ) set ) = b : ( ( real ) ( V28() real ext-real ) number ) ) ;

theorem :: TOPREALA:30
for a, b, r, s being ( ( real ) ( V28() real ext-real ) number ) holds closed_inside_of_rectangle (a : ( ( real ) ( V28() real ext-real ) number ) ,b : ( ( real ) ( V28() real ext-real ) number ) ,r : ( ( real ) ( V28() real ext-real ) number ) ,s : ( ( real ) ( V28() real ext-real ) number ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) = product ((1 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) --> ([.a : ( ( real ) ( V28() real ext-real ) number ) ,b : ( ( real ) ( V28() real ext-real ) number ) .] : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ,[.r : ( ( real ) ( V28() real ext-real ) number ) ,s : ( ( real ) ( V28() real ext-real ) number ) .] : ( ( ) ( V176() V177() V178() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) )) : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined Function-like ) set ) : ( ( ) ( ) set ) ;

theorem :: TOPREALA:31
for a, b, r, s being ( ( real ) ( V28() real ext-real ) number ) st a : ( ( real ) ( V28() real ext-real ) number ) <= b : ( ( real ) ( V28() real ext-real ) number ) & r : ( ( real ) ( V28() real ext-real ) number ) <= s : ( ( real ) ( V28() real ext-real ) number ) holds
|[a : ( ( real ) ( V28() real ext-real ) number ) ,r : ( ( real ) ( V28() real ext-real ) number ) ]| : ( ( ) ( Relation-like NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) -defined Function-like non empty V30() V37(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V166() V167() V168() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) : ( ( ) ( non empty ) set ) ) in closed_inside_of_rectangle (a : ( ( real ) ( V28() real ext-real ) number ) ,b : ( ( real ) ( V28() real ext-real ) number ) ,r : ( ( real ) ( V28() real ext-real ) number ) ,s : ( ( real ) ( V28() real ext-real ) number ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;

definition
let a, b, c, d be ( ( real ) ( V28() real ext-real ) number ) ;
func Trectangle (a,b,c,d) -> ( ( ) ( TopSpace-like constituted-Functions constituted-FinSeqs ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) ) equals :: TOPREALA:def 1
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) | (closed_inside_of_rectangle (a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ,c : ( ( ) ( ) Element of a : ( ( ) ( ) set ) ) ,d : ( ( real ) ( V28() real ext-real ) set ) )) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) : ( ( strict ) ( strict TopSpace-like constituted-Functions constituted-FinSeqs ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) ) ;
end;

theorem :: TOPREALA:32
for a, b, r, s being ( ( real ) ( V28() real ext-real ) number ) st a : ( ( real ) ( V28() real ext-real ) number ) <= b : ( ( real ) ( V28() real ext-real ) number ) & r : ( ( real ) ( V28() real ext-real ) number ) <= s : ( ( real ) ( V28() real ext-real ) number ) holds
not Trectangle (a : ( ( real ) ( V28() real ext-real ) number ) ,b : ( ( real ) ( V28() real ext-real ) number ) ,r : ( ( real ) ( V28() real ext-real ) number ) ,s : ( ( real ) ( V28() real ext-real ) number ) ) : ( ( ) ( TopSpace-like constituted-Functions constituted-FinSeqs ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) ) is empty ;

registration
let a, c be ( ( real non positive ) ( V28() real ext-real non positive ) number ) ;
let b, d be ( ( real non negative ) ( V28() real ext-real non negative ) number ) ;
cluster Trectangle (a : ( ( real non positive ) ( V28() real ext-real non positive ) set ) ,b : ( ( real non negative ) ( V28() real ext-real non negative ) set ) ,c : ( ( real non positive ) ( V28() real ext-real non positive ) set ) ,d : ( ( real non negative ) ( V28() real ext-real non negative ) set ) ) : ( ( ) ( TopSpace-like constituted-Functions constituted-FinSeqs ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) ) -> non empty ;
end;

definition
func R2Homeomorphism -> ( ( Function-like quasi_total ) ( Relation-like the carrier of [:R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ,R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) means :: TOPREALA:def 2
 for x, y being ( ( real ) ( V28() real ext-real ) number ) holds it : ( ( ) ( ) set ) . [x : ( ( real ) ( V28() real ext-real ) number ) ,y : ( ( real ) ( V28() real ext-real ) number ) ] : ( ( ) ( ) set ) : ( ( ) ( ) set ) = <*x : ( ( real ) ( V28() real ext-real ) number ) ,y : ( ( real ) ( V28() real ext-real ) number ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) -defined Function-like non empty V30() V37(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) set ) ;
end;

theorem :: TOPREALA:33
for A, B being ( ( ) ( V176() V177() V178() ) Subset of ( ( ) ( ) set ) ) holds R2Homeomorphism : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ,R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: [:A : ( ( ) ( V176() V177() V178() ) Subset of ( ( ) ( ) set ) ) ,B : ( ( ) ( V176() V177() V178() ) Subset of ( ( ) ( ) set ) ) :] : ( ( ) ( Relation-like V166() V167() V168() ) set ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) = product ((1 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) --> (A : ( ( ) ( V176() V177() V178() ) Subset of ( ( ) ( ) set ) ) ,B : ( ( ) ( V176() V177() V178() ) Subset of ( ( ) ( ) set ) ) )) : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined Function-like ) set ) : ( ( ) ( ) set ) ;

theorem :: TOPREALA:34
R2Homeomorphism : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ,R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism ;

theorem :: TOPREALA:35
for a, b, r, s being ( ( real ) ( V28() real ext-real ) number ) st a : ( ( real ) ( V28() real ext-real ) number ) <= b : ( ( real ) ( V28() real ext-real ) number ) & r : ( ( real ) ( V28() real ext-real ) number ) <= s : ( ( real ) ( V28() real ext-real ) number ) holds
R2Homeomorphism : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ,R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) | the carrier of [:(Closed-Interval-TSpace (a : ( ( real ) ( V28() real ext-real ) number ) ,b : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) ,(Closed-Interval-TSpace (r : ( ( real ) ( V28() real ext-real ) number ) ,s : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( Function-like ) ( Relation-like the carrier of [:R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ,R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of [:(Closed-Interval-TSpace (b1 : ( ( real ) ( V28() real ext-real ) number ) ,b2 : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) ,(Closed-Interval-TSpace (b3 : ( ( real ) ( V28() real ext-real ) number ) ,b4 : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of [:R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ,R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [: the carrier of [:R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ,R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is ( ( Function-like quasi_total ) ( Relation-like the carrier of [:(Closed-Interval-TSpace (b1 : ( ( real ) ( V28() real ext-real ) number ) ,b2 : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) ,(Closed-Interval-TSpace (b3 : ( ( real ) ( V28() real ext-real ) number ) ,b4 : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (Trectangle (b1 : ( ( real ) ( V28() real ext-real ) number ) ,b2 : ( ( real ) ( V28() real ext-real ) number ) ,b3 : ( ( real ) ( V28() real ext-real ) number ) ,b4 : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( ) ( TopSpace-like constituted-Functions constituted-FinSeqs ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) ;

theorem :: TOPREALA:36
for a, b, r, s being ( ( real ) ( V28() real ext-real ) number ) st a : ( ( real ) ( V28() real ext-real ) number ) <= b : ( ( real ) ( V28() real ext-real ) number ) & r : ( ( real ) ( V28() real ext-real ) number ) <= s : ( ( real ) ( V28() real ext-real ) number ) holds
for h being ( ( Function-like quasi_total ) ( Relation-like the carrier of [:(Closed-Interval-TSpace (b1 : ( ( real ) ( V28() real ext-real ) number ) ,b2 : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) ,(Closed-Interval-TSpace (b3 : ( ( real ) ( V28() real ext-real ) number ) ,b4 : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (Trectangle (b1 : ( ( real ) ( V28() real ext-real ) number ) ,b2 : ( ( real ) ( V28() real ext-real ) number ) ,b3 : ( ( real ) ( V28() real ext-real ) number ) ,b4 : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( ) ( TopSpace-like constituted-Functions constituted-FinSeqs ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) st h : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:(Closed-Interval-TSpace (b1 : ( ( real ) ( V28() real ext-real ) number ) ,b2 : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) ,(Closed-Interval-TSpace (b3 : ( ( real ) ( V28() real ext-real ) number ) ,b4 : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (Trectangle (b1 : ( ( real ) ( V28() real ext-real ) number ) ,b2 : ( ( real ) ( V28() real ext-real ) number ) ,b3 : ( ( real ) ( V28() real ext-real ) number ) ,b4 : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( ) ( TopSpace-like constituted-Functions constituted-FinSeqs ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) = R2Homeomorphism : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ,R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) | the carrier of [:(Closed-Interval-TSpace (a : ( ( real ) ( V28() real ext-real ) number ) ,b : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) ,(Closed-Interval-TSpace (r : ( ( real ) ( V28() real ext-real ) number ) ,s : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( Function-like ) ( Relation-like the carrier of [:R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ,R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of [:(Closed-Interval-TSpace (b1 : ( ( real ) ( V28() real ext-real ) number ) ,b2 : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) ,(Closed-Interval-TSpace (b3 : ( ( real ) ( V28() real ext-real ) number ) ,b4 : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of [:R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ,R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [: the carrier of [:R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ,R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) holds
h : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:(Closed-Interval-TSpace (b1 : ( ( real ) ( V28() real ext-real ) number ) ,b2 : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) ,(Closed-Interval-TSpace (b3 : ( ( real ) ( V28() real ext-real ) number ) ,b4 : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (Trectangle (b1 : ( ( real ) ( V28() real ext-real ) number ) ,b2 : ( ( real ) ( V28() real ext-real ) number ) ,b3 : ( ( real ) ( V28() real ext-real ) number ) ,b4 : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( ) ( TopSpace-like constituted-Functions constituted-FinSeqs ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) is being_homeomorphism ;

theorem :: TOPREALA:37
for a, b, r, s being ( ( real ) ( V28() real ext-real ) number ) st a : ( ( real ) ( V28() real ext-real ) number ) <= b : ( ( real ) ( V28() real ext-real ) number ) & r : ( ( real ) ( V28() real ext-real ) number ) <= s : ( ( real ) ( V28() real ext-real ) number ) holds
[:(Closed-Interval-TSpace (a : ( ( real ) ( V28() real ext-real ) number ) ,b : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) ,(Closed-Interval-TSpace (r : ( ( real ) ( V28() real ext-real ) number ) ,s : ( ( real ) ( V28() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V227() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V227() ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) , Trectangle (a : ( ( real ) ( V28() real ext-real ) number ) ,b : ( ( real ) ( V28() real ext-real ) number ) ,r : ( ( real ) ( V28() real ext-real ) number ) ,s : ( ( real ) ( V28() real ext-real ) number ) ) : ( ( ) ( TopSpace-like constituted-Functions constituted-FinSeqs ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) : ( ( V241() ) ( non empty TopSpace-like V123() constituted-Functions constituted-FinSeqs V229() V230() V231() V232() V233() V234() V235() V241() ) L16()) ) are_homeomorphic ;

theorem :: TOPREALA:38
for a, b, r, s being ( ( real ) ( V28() real ext-real ) number ) st a : ( ( real ) ( V28() real ext-real ) number ) <= b : ( ( real ) ( V28() real ext-real ) number ) & r : ( ( real ) ( V28() real ext-real ) number ) <= s : ( ( real ) ( V28() real ext-real ) number ) holds
for A being ( ( ) ( V176() V177() V178() ) Subset of )
for B being ( ( ) ( V176() V177() V178() ) Subset of ) holds product ((1 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) --> (A : ( ( ) ( V176() V177() V178() ) Subset of ) ,B : ( ( ) ( V176() V177() V178() ) Subset of ) )) : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined Function-like ) set ) : ( ( ) ( ) set ) is ( ( ) ( ) Subset of ) ;

theorem :: TOPREALA:39
for a, b, r, s being ( ( real ) ( V28() real ext-real ) number ) st a : ( ( real ) ( V28() real ext-real ) number ) <= b : ( ( real ) ( V28() real ext-real ) number ) & r : ( ( real ) ( V28() real ext-real ) number ) <= s : ( ( real ) ( V28() real ext-real ) number ) holds
for A being ( ( open ) ( open V176() V177() V178() ) Subset of )
for B being ( ( open ) ( open V176() V177() V178() ) Subset of ) holds product ((1 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) --> (A : ( ( open ) ( open V176() V177() V178() ) Subset of ) ,B : ( ( open ) ( open V176() V177() V178() ) Subset of ) )) : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined Function-like ) set ) : ( ( ) ( ) set ) is ( ( open ) ( open ) Subset of ) ;

theorem :: TOPREALA:40
for a, b, r, s being ( ( real ) ( V28() real ext-real ) number ) st a : ( ( real ) ( V28() real ext-real ) number ) <= b : ( ( real ) ( V28() real ext-real ) number ) & r : ( ( real ) ( V28() real ext-real ) number ) <= s : ( ( real ) ( V28() real ext-real ) number ) holds
for A being ( ( closed ) ( closed V176() V177() V178() ) Subset of )
for B being ( ( closed ) ( closed V176() V177() V178() ) Subset of ) holds product ((1 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty natural V28() real ext-real positive non negative integer V110() V176() V177() V178() V179() V180() V181() ) Element of NAT : ( ( ) ( V176() V177() V178() V179() V180() V181() V182() ) Element of bool REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) : ( ( ) ( ) set ) ) ) ) --> (A : ( ( closed ) ( closed V176() V177() V178() ) Subset of ) ,B : ( ( closed ) ( closed V176() V177() V178() ) Subset of ) )) : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V30() V176() V177() V178() V182() ) set ) -defined Function-like ) set ) : ( ( ) ( ) set ) is ( ( closed ) ( closed ) Subset of ) ;