:: JORDAN24 semantic presentation

begin

definition
let n be ( ( ) ( natural complex real ext-real integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ;
let A be ( ( ) ( ) Subset of ) ;
let a, b be ( ( ) ( V40(n : ( ( ) ( natural complex real ext-real integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) ;
pred a,b realize-max-dist-in A means :: JORDAN24:def 1
( a : ( ( ) ( ) Element of K6(K6(n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) in A : ( ( Function-like quasi_total ) ( V16() V19(K7(n : ( ( ) ( ) TopGrStr ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ) V20(n : ( ( ) ( ) TopGrStr ) ) Function-like quasi_total ) Element of K6(K7(K7(n : ( ( ) ( ) TopGrStr ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) & b : ( ( Function-like quasi_total ) ( V16() V19(K7(n : ( ( ) ( ) TopGrStr ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ) V20(n : ( ( ) ( ) TopGrStr ) ) Function-like quasi_total ) Element of K6(K7(K7(n : ( ( ) ( ) TopGrStr ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) in A : ( ( Function-like quasi_total ) ( V16() V19(K7(n : ( ( ) ( ) TopGrStr ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ) V20(n : ( ( ) ( ) TopGrStr ) ) Function-like quasi_total ) Element of K6(K7(K7(n : ( ( ) ( ) TopGrStr ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) & ( for x, y being ( ( ) ( V40(n : ( ( ) ( ) TopGrStr ) ) V98() V141() ) Point of ( ( ) ( ) set ) ) st x : ( ( ) ( V40(n : ( ( ) ( natural complex real ext-real integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) in A : ( ( Function-like quasi_total ) ( V16() V19(K7(n : ( ( ) ( ) TopGrStr ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ) V20(n : ( ( ) ( ) TopGrStr ) ) Function-like quasi_total ) Element of K6(K7(K7(n : ( ( ) ( ) TopGrStr ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) & y : ( ( ) ( V40(n : ( ( ) ( natural complex real ext-real integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) in A : ( ( Function-like quasi_total ) ( V16() V19(K7(n : ( ( ) ( ) TopGrStr ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ) V20(n : ( ( ) ( ) TopGrStr ) ) Function-like quasi_total ) Element of K6(K7(K7(n : ( ( ) ( ) TopGrStr ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) holds
dist (a : ( ( ) ( ) Element of K6(K6(n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,b : ( ( Function-like quasi_total ) ( V16() V19(K7(n : ( ( ) ( ) TopGrStr ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ) V20(n : ( ( ) ( ) TopGrStr ) ) Function-like quasi_total ) Element of K6(K7(K7(n : ( ( ) ( ) TopGrStr ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ,n : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) >= dist (x : ( ( ) ( V40(n : ( ( ) ( natural complex real ext-real integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( V40(n : ( ( ) ( natural complex real ext-real integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) ) );
end;

theorem :: JORDAN24:1
for C being ( ( non empty compact ) ( non empty compact ) Subset of ) ex p1, p2 being ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) st p1 : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) realize-max-dist-in C : ( ( non empty compact ) ( non empty compact ) Subset of ) ;

definition
let M be ( ( non empty ) ( non empty ) MetrStruct ) ;
let f be ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (TopSpaceMetr M : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TopSpaceMetr M : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of (TopSpaceMetr M : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
attr f is isometric means :: JORDAN24:def 2
 ex g being ( ( Function-like quasi_total isometric ) ( non empty V16() V19( the carrier of M : ( ( ) ( ) TopGrStr ) : ( ( ) ( ) set ) ) V20( the carrier of M : ( ( ) ( ) TopGrStr ) : ( ( ) ( ) set ) ) Function-like V26( the carrier of M : ( ( ) ( ) TopGrStr ) : ( ( ) ( ) set ) ) quasi_total isometric ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st g : ( ( Function-like quasi_total isometric ) ( non empty V16() V19( the carrier of M : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) V20( the carrier of M : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of M : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) quasi_total isometric ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( V16() V19(K7(M : ( ( ) ( ) TopGrStr ) ,M : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ) V20(M : ( ( ) ( ) TopGrStr ) ) Function-like quasi_total ) Element of K6(K7(K7(M : ( ( ) ( ) TopGrStr ) ,M : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ,M : ( ( ) ( ) TopGrStr ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) ;
end;

registration
let M be ( ( non empty ) ( non empty ) MetrStruct ) ;
cluster non empty V16() V19( the carrier of (TopSpaceMetr M : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TopSpaceMetr M : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of (TopSpaceMetr M : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total onto isometric for ( ( ) ( ) Element of K6(K7( the carrier of (TopSpaceMetr M : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (TopSpaceMetr M : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) ;
end;

registration
let M be ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle ) MetrSpace) ;
cluster Function-like quasi_total isometric -> Function-like quasi_total continuous for ( ( ) ( ) Element of K6(K7( the carrier of (TopSpaceMetr M : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (TopSpaceMetr M : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) ;
end;

registration
let M be ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle ) MetrSpace) ;
cluster Function-like quasi_total onto isometric -> Function-like quasi_total being_homeomorphism for ( ( ) ( ) Element of K6(K7( the carrier of (TopSpaceMetr M : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (TopSpaceMetr M : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) ;
end;

definition
let a be ( ( ) ( complex real ext-real ) Real) ;
func Rotate a -> ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) means :: JORDAN24:def 3
 for p being ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) holds it : ( ( ) ( ) set ) . p : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) = |[(Re (Rotate (((p : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) `1) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) + ((p : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) * <i> : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ,a : ( ( non empty ) ( non empty ) MetrStruct ) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( V149() V155() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) ,(Im (Rotate (((p : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) `1) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) + ((p : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) `2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) * <i> : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ,a : ( ( non empty ) ( non empty ) MetrStruct ) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( V149() V155() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) ]| : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: JORDAN24:2
for a being ( ( ) ( complex real ext-real ) Real)
for f being ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (TopSpaceMetr (Euclid 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TopSpaceMetr (Euclid 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of (TopSpaceMetr (Euclid 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (TopSpaceMetr (Euclid 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TopSpaceMetr (Euclid 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of (TopSpaceMetr (Euclid 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = Rotate a : ( ( ) ( complex real ext-real ) Real) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
( f : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (TopSpaceMetr (Euclid 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TopSpaceMetr (Euclid 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of (TopSpaceMetr (Euclid 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is onto & f : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (TopSpaceMetr (Euclid 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TopSpaceMetr (Euclid 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of (TopSpaceMetr (Euclid 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict Reflexive discerning symmetric triangle ) ( non empty strict Reflexive discerning symmetric triangle ) MetrStruct ) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is isometric ) ;

theorem :: JORDAN24:3
for p1, p2 being ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) )
for P being ( ( ) ( ) Subset of )
for A, B, D being ( ( real ) ( complex real ext-real ) number ) st p1 : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) realize-max-dist-in P : ( ( ) ( ) Subset of ) holds
(AffineMap (A : ( ( real ) ( complex real ext-real ) number ) ,B : ( ( real ) ( complex real ext-real ) number ) ,A : ( ( real ) ( complex real ext-real ) number ) ,D : ( ( real ) ( complex real ext-real ) number ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) . p1 : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) ,(AffineMap (A : ( ( real ) ( complex real ext-real ) number ) ,B : ( ( real ) ( complex real ext-real ) number ) ,A : ( ( real ) ( complex real ext-real ) number ) ,D : ( ( real ) ( complex real ext-real ) number ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) . p2 : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) realize-max-dist-in (AffineMap (A : ( ( real ) ( complex real ext-real ) number ) ,B : ( ( real ) ( complex real ext-real ) number ) ,A : ( ( real ) ( complex real ext-real ) number ) ,D : ( ( real ) ( complex real ext-real ) number ) )) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) .: P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: JORDAN24:4
for p1, p2 being ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) )
for P being ( ( ) ( ) Subset of )
for A being ( ( ) ( complex real ext-real ) Real) st p1 : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) realize-max-dist-in P : ( ( ) ( ) Subset of ) holds
(Rotate A : ( ( ) ( complex real ext-real ) Real) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . p1 : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) ,(Rotate A : ( ( ) ( complex real ext-real ) Real) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . p2 : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) realize-max-dist-in (Rotate A : ( ( ) ( complex real ext-real ) Real) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: JORDAN24:5
for z being ( ( complex ) ( complex ) number )
for r being ( ( ) ( complex real ext-real ) Real) holds Rotate (z : ( ( complex ) ( complex ) number ) ,(- r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( V149() V155() ) set ) ) = Rotate (z : ( ( complex ) ( complex ) number ) ,((2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) - r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( V149() V155() ) set ) ) ;

theorem :: JORDAN24:6
for r being ( ( ) ( complex real ext-real ) Real) holds Rotate (- r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = Rotate ((2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) ) : ( ( ) ( non empty complex real ext-real positive non negative ) Element of REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) - r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;

theorem :: JORDAN24:7
for C being ( ( being_simple_closed_curve ) ( non empty compact being_simple_closed_curve ) Simple_closed_curve) ex f being ( ( ) ( non empty V16() V19( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like one-to-one V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) quasi_total onto bijective continuous being_homeomorphism ) Homeomorphism of TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) ) st |[(- 1 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty complex real ext-real non positive negative integer ) Element of REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) ,0 : ( ( ) ( empty natural complex real ext-real non positive non negative V16() non-empty empty-yielding integer V102() V149() V150() V151() V152() V153() V154() V155() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ]| : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) ,|[1 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ,0 : ( ( ) ( empty natural complex real ext-real non positive non negative V16() non-empty empty-yielding integer V102() V149() V150() V151() V152() V153() V154() V155() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ]| : ( ( ) ( V40(2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) V98() V141() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) realize-max-dist-in f : ( ( ) ( non empty V16() V19( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like one-to-one V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) quasi_total onto bijective continuous being_homeomorphism ) Homeomorphism of TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) ) .: C : ( ( being_simple_closed_curve ) ( non empty compact being_simple_closed_curve ) Simple_closed_curve) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

definition
let T1, T2 be ( ( ) ( ) TopStruct ) ;
let f be ( ( Function-like quasi_total ) ( V16() V19( the carrier of T1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) V20( the carrier of T2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ;
attr f is closed means :: JORDAN24:def 4
 for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is closed holds
f : ( ( ) ( ) Element of K6(K6(T1 : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) .: A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of T2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is closed ;
end;

theorem :: JORDAN24:8
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is one-to-one & f : ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is onto holds
( f : ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism iff f : ( ( Function-like quasi_total continuous ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is closed ) ;

theorem :: JORDAN24:9
for X being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) holds
( A : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ` : ( ( ) ( ) Element of K6(b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = {} : ( ( ) ( empty V16() non-empty empty-yielding V149() V150() V151() V152() V153() V154() V155() ) set ) iff A : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) = X : ( ( ) ( ) set ) ) ;

theorem :: JORDAN24:10
for T1, T2 being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism holds
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is connected holds
f : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is connected ;

theorem :: JORDAN24:11
for T1, T2 being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism holds
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is a_component holds
f : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is a_component ;

theorem :: JORDAN24:12
for T1, T2 being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) holds f : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) | A : ( ( ) ( ) Subset of ) : ( ( Function-like ) ( V16() V19(b4 : ( ( ) ( ) Subset of ) ) V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like ) Element of K6(K7( 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 ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) is ( ( Function-like quasi_total ) ( V16() V19( the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) V20( the carrier of (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | (b3 : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: b4 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ;

theorem :: JORDAN24:13
for T1, T2 being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous holds
for A being ( ( ) ( ) Subset of )
for g being ( ( Function-like quasi_total ) ( V16() V19( the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) V20( the carrier of (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | (b3 : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: b4 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st g : ( ( Function-like quasi_total ) ( V16() V19( the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) V20( the carrier of (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | (b3 : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: b4 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) = f : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) | A : ( ( ) ( ) Subset of ) : ( ( Function-like ) ( V16() V19(b4 : ( ( ) ( ) Subset of ) ) V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like ) Element of K6(K7( 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 ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) holds
g : ( ( Function-like quasi_total ) ( V16() V19( the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) V20( the carrier of (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | (b3 : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: b4 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is continuous ;

theorem :: JORDAN24:14
for T1, T2 being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism holds
for A being ( ( ) ( ) Subset of )
for g being ( ( Function-like quasi_total ) ( V16() V19( the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) V20( the carrier of (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | (b3 : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: b4 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st g : ( ( Function-like quasi_total ) ( V16() V19( the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) V20( the carrier of (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | (b3 : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: b4 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) = f : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) | A : ( ( ) ( ) Subset of ) : ( ( Function-like ) ( V16() V19(b4 : ( ( ) ( ) Subset of ) ) V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like ) Element of K6(K7( 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 ) ) : ( ( ) ( V16() ) set ) ) : ( ( ) ( ) set ) ) holds
g : ( ( Function-like quasi_total ) ( V16() V19( the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) V20( the carrier of (b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | (b3 : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: b4 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is being_homeomorphism ;

theorem :: JORDAN24:15
for T1, T2 being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism holds
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is_a_component_of B : ( ( ) ( ) Subset of ) holds
f : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is_a_component_of f : ( ( Function-like quasi_total ) ( non empty V16() V19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V20( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: JORDAN24:16
for S being ( ( ) ( ) Subset of )
for f being ( ( ) ( non empty V16() V19( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like one-to-one V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) quasi_total onto bijective continuous being_homeomorphism ) Homeomorphism of TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) ) st S : ( ( ) ( ) Subset of ) is Jordan holds
f : ( ( ) ( non empty V16() V19( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) V20( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) Function-like one-to-one V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) quasi_total onto bijective continuous being_homeomorphism ) Homeomorphism of TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) ) .: S : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural complex real ext-real positive non negative integer V102() V149() V150() V151() V152() V153() V154() ) Element of NAT : ( ( ) ( V149() V150() V151() V152() V153() V154() V155() ) Element of K6(REAL : ( ( ) ( V149() V150() V151() V155() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V173() ) ( non empty TopSpace-like V115() V161() V162() V163() V164() V165() V166() V167() V173() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is Jordan ;