JORDAN1C

:: JORDAN1C semantic presentation

begin

for S being ( ( ) ( ) Subset of ) st S : ( ( ) ( ) Subset of ) is bounded holds
proj1 : ( ( V24() V46( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) , REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) V23( REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) V24() V46( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) , REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) V145() V146() V147() V203( TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) ) ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ,REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( V145() V146() V147() ) set ) ) : ( ( ) ( ) set ) ) .: S : ( ( ) ( ) Subset of ) : ( ( ) ( V155() V156() V157() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) is real-bounded ;

theorem :: JORDAN1C:4

for C1 being ( ( non empty compact ) ( non empty closed compact bounded ) Subset of )
for C2, S being ( ( non empty ) ( non empty ) Subset of ) st S : ( ( non empty ) ( non empty ) Subset of ) = C1 : ( ( non empty compact ) ( non empty closed compact bounded ) Subset of ) \/ C2 : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) & not proj1 : ( ( V24() V46( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) , REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) V23( REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) V24() V46( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) , REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) V145() V146() V147() V203( TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) ) ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ,REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( V145() V146() V147() ) set ) ) : ( ( ) ( ) set ) ) .: C2 : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( non empty V155() V156() V157() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) is empty & proj1 : ( ( V24() V46( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) , REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) V23( REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) V24() V46( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) , REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) V145() V146() V147() V203( TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) ) ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ,REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( V145() V146() V147() ) set ) ) : ( ( ) ( ) set ) ) .: C2 : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( non empty V155() V156() V157() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) is bounded_below holds
W-bound S : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) = min ((W-bound C1 : ( ( non empty compact ) ( non empty closed compact bounded ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ,(W-bound C2 : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: JORDAN1C:5

for p being ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) )
for X being ( ( ) ( ) Subset of ) st p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) in X : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Subset of ) is bounded holds
( W-bound X : ( ( ) ( ) Subset of ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) <= p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) & p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) <= E-bound X : ( ( ) ( ) Subset of ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) & S-bound X : ( ( ) ( ) Subset of ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) <= p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) & p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) <= N-bound X : ( ( ) ( ) Subset of ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ) ;

theorem :: JORDAN1C:6

for C being ( ( compact ) ( closed compact bounded ) Subset of ) st BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) <> {} : ( ( ) ( empty V155() V156() V157() V158() V159() V160() V161() ) set ) holds
W-bound C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) <= W-bound (BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ;

theorem :: JORDAN1C:7

for C being ( ( compact ) ( closed compact bounded ) Subset of ) st BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) <> {} : ( ( ) ( empty V155() V156() V157() V158() V159() V160() V161() ) set ) holds
E-bound C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) >= E-bound (BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ;

theorem :: JORDAN1C:8

for C being ( ( compact ) ( closed compact bounded ) Subset of ) st BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) <> {} : ( ( ) ( empty V155() V156() V157() V158() V159() V160() V161() ) set ) holds
S-bound C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) <= S-bound (BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ;

theorem :: JORDAN1C:9

for C being ( ( compact ) ( closed compact bounded ) Subset of ) st BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) <> {} : ( ( ) ( empty V155() V156() V157() V158() V159() V160() V161() ) set ) holds
N-bound C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) >= N-bound (BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ;

theorem :: JORDAN1C:10

theorem :: JORDAN1C:11

for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) )
for p being ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) )
for C being ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of )
for I being ( ( integer ) ( V11() real ext-real integer ) Integer) st p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) in BDD C : ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) & I : ( ( integer ) ( V11() real ext-real integer ) Integer) = [\(((((p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) `1) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) - (W-bound C : ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) / ((E-bound C : ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) - (W-bound C : ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) * (2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) |^ n : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) + 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) /] : ( ( integer ) ( V11() real ext-real integer ) set ) holds
I : ( ( integer ) ( V11() real ext-real integer ) Integer) + 1 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real integer ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) <= len (Gauge (C : ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of ) ,n : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V19() V21() V22( NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) V23(K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) V24() FinSequence-like tabular V188() V189() ) FinSequence of K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: JORDAN1C:12

for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) )
for p being ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) )
for C being ( ( compact non horizontal ) ( non empty closed compact bounded non horizontal ) Subset of )
for J being ( ( integer ) ( V11() real ext-real integer ) Integer) st p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) in BDD C : ( ( compact non horizontal ) ( non empty closed compact bounded non horizontal ) Subset of ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) & J : ( ( integer ) ( V11() real ext-real integer ) Integer) = [\(((((p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) `2) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) - (S-bound C : ( ( compact non horizontal ) ( non empty closed compact bounded non horizontal ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) / ((N-bound C : ( ( compact non horizontal ) ( non empty closed compact bounded non horizontal ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) - (S-bound C : ( ( compact non horizontal ) ( non empty closed compact bounded non horizontal ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) * (2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) |^ n : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) + 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) /] : ( ( integer ) ( V11() real ext-real integer ) set ) holds
( 1 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) < J : ( ( integer ) ( V11() real ext-real integer ) Integer) & J : ( ( integer ) ( V11() real ext-real integer ) Integer) + 1 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real integer ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) <= width (Gauge (C : ( ( compact non horizontal ) ( non empty closed compact bounded non horizontal ) Subset of ) ,n : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V19() V21() V22( NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) V23(K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) V24() FinSequence-like tabular V188() V189() ) FinSequence of K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: JORDAN1C:13

theorem :: JORDAN1C:14

theorem :: JORDAN1C:15

theorem :: JORDAN1C:16

theorem :: JORDAN1C:17

for C being ( ( closed ) ( closed ) Subset of )
for p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in BDD C : ( ( closed ) ( closed ) Subset of ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) holds
ex r being ( ( ) ( V11() real ext-real ) Real) st
( r : ( ( ) ( V11() real ext-real ) Real) > 0 : ( ( ) ( empty ordinal natural V11() real ext-real non positive non negative integer V108() V155() V156() V157() V158() V159() V160() V161() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) & Ball (p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( ) Element of K6( the carrier of (Euclid 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict Reflexive discerning V97() triangle ) ( non empty strict Reflexive discerning V97() triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) c= BDD C : ( ( closed ) ( closed ) Subset of ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: JORDAN1C:18

for C being ( ( being_simple_closed_curve ) ( non empty closed V83( TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) ) compact bounded being_simple_closed_curve non horizontal non vertical ) Simple_closed_curve)
for n, i, j being ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) )
for p, q being ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) )
for r being ( ( real ) ( V11() real ext-real ) number ) st dist (((Gauge (C : ( ( being_simple_closed_curve ) ( non empty closed V83( TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) ) compact bounded being_simple_closed_curve non horizontal non vertical ) Simple_closed_curve) ,n : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V19() V21() V22( NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) V23(K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) V24() FinSequence-like tabular V188() V189() V190() V191() ) FinSequence of K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) * (1 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) ,((Gauge (C : ( ( being_simple_closed_curve ) ( non empty closed V83( TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) ) compact bounded being_simple_closed_curve non horizontal non vertical ) Simple_closed_curve) ,n : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V19() V21() V22( NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) V23(K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) V24() FinSequence-like tabular V188() V189() V190() V191() ) FinSequence of K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) * (1 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) < r : ( ( real ) ( V11() real ext-real ) number ) & dist (((Gauge (C : ( ( being_simple_closed_curve ) ( non empty closed V83( TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) ) compact bounded being_simple_closed_curve non horizontal non vertical ) Simple_closed_curve) ,n : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V19() V21() V22( NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) V23(K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) V24() FinSequence-like tabular V188() V189() V190() V191() ) FinSequence of K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) * (1 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) ,((Gauge (C : ( ( being_simple_closed_curve ) ( non empty closed V83( TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) ) compact bounded being_simple_closed_curve non horizontal non vertical ) Simple_closed_curve) ,n : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V19() V21() V22( NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) V23(K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) V24() FinSequence-like tabular V188() V189() V190() V191() ) FinSequence of K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) * (2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) < r : ( ( real ) ( V11() real ext-real ) number ) & p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) in cell ((Gauge (C : ( ( being_simple_closed_curve ) ( non empty closed V83( TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) ) compact bounded being_simple_closed_curve non horizontal non vertical ) Simple_closed_curve) ,n : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V19() V21() V22( NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) V23(K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) V24() FinSequence-like tabular V188() V189() V190() V191() ) FinSequence of K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) ,i : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ,j : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) & q : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) in cell ((Gauge (C : ( ( being_simple_closed_curve ) ( non empty closed V83( TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) ) compact bounded being_simple_closed_curve non horizontal non vertical ) Simple_closed_curve) ,n : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V19() V21() V22( NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) V23(K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) V24() FinSequence-like tabular V188() V189() V190() V191() ) FinSequence of K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) ,i : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ,j : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) & 1 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) & i : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) <= len (Gauge (C : ( ( being_simple_closed_curve ) ( non empty closed V83( TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) ) compact bounded being_simple_closed_curve non horizontal non vertical ) Simple_closed_curve) ,n : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V19() V21() V22( NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) V23(K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) V24() FinSequence-like tabular V188() V189() V190() V191() ) FinSequence of K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) & 1 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) <= j : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) & j : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) <= width (Gauge (C : ( ( being_simple_closed_curve ) ( non empty closed V83( TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) ) compact bounded being_simple_closed_curve non horizontal non vertical ) Simple_closed_curve) ,n : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( tabular ) ( V19() V21() V22( NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) V23(K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) V24() FinSequence-like tabular V188() V189() V190() V191() ) FinSequence of K333( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) )) ) : ( ( ) ( ordinal natural V11() real ext-real non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) holds
dist (p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) ,q : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) < 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) * r : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ;

theorem :: JORDAN1C:19

for p being ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) )
for C being ( ( compact ) ( closed compact bounded ) Subset of ) st p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) in BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) holds
p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) <> N-bound (BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ;

theorem :: JORDAN1C:20

for p being ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) )
for C being ( ( compact ) ( closed compact bounded ) Subset of ) st p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) in BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) holds
p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) <> E-bound (BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ;

theorem :: JORDAN1C:21

for p being ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) )
for C being ( ( compact ) ( closed compact bounded ) Subset of ) st p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) in BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) holds
p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) <> S-bound (BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ;

theorem :: JORDAN1C:22

for p being ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) )
for C being ( ( compact ) ( closed compact bounded ) Subset of ) st p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) in BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) holds
p : ( ( ) ( V41(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V147() ) Point of ( ( ) ( non empty V27() ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) <> W-bound (BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) ;

theorem :: JORDAN1C:23

theorem :: JORDAN1C:24

for C being ( ( ) ( ) Subset of ) st C : ( ( ) ( ) Subset of ) is bounded holds
not UBD C : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative integer V108() V155() V156() V157() V158() V159() V160() ) Element of NAT : ( ( ) ( V155() V156() V157() V158() V159() V160() V161() ) Element of K6(REAL : ( ( ) ( non empty V34() V155() V156() V157() V161() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V121() V167() V168() V169() V170() V171() V172() V173() strict V180() V181() ) L15()) : ( ( ) ( non empty V27() ) set ) ) : ( ( ) ( ) set ) ) is empty ;