:: JORDAN18 semantic presentation

begin

theorem :: JORDAN18:1
for a, b being ( ( real ) ( V11() real ext-real ) number ) holds (a : ( ( real ) ( V11() real ext-real ) number ) - b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ^2 : ( ( ) ( V11() real ext-real ) set ) = (b : ( ( real ) ( V11() real ext-real ) number ) - a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ^2 : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: JORDAN18:2
for S, T being ( ( non empty ) ( non empty ) TopStruct )
for f being ( ( Function-like V33( the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( V19() V22( the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V33( the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) st f : ( ( Function-like V33( the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( V19() V22( the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V33( the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism & A : ( ( ) ( ) Subset of ) is compact holds
f : ( ( Function-like V33( the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( V19() V22( the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V33( the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) is compact ;

theorem :: JORDAN18:3
for a being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds proj2 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) V23( REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) Element of bool [: the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .: (north_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V142() V143() V144() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) is bounded_below ;

theorem :: JORDAN18:4
for a being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds proj2 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) V23( REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) Element of bool [: the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .: (south_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V142() V143() V144() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) is bounded_above ;

theorem :: JORDAN18:5
for a being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds proj1 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) V23( REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) Element of bool [: the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .: (west_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V142() V143() V144() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) is bounded_above ;

theorem :: JORDAN18:6
for a being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds proj1 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) V23( REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) Element of bool [: the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .: (east_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V142() V143() V144() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) is bounded_below ;

registration
let a be ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ;
cluster proj2 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) V23( REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) Element of bool [: the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .: (north_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster proj2 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) V23( REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) Element of bool [: the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .: (south_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster proj1 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) V23( REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) Element of bool [: the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .: (west_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -> non empty ;
cluster proj1 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) V23( REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) Element of bool [: the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .: (east_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -> non empty ;
end;

theorem :: JORDAN18:7
for a being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds lower_bound (proj2 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) V23( REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) Element of bool [: the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .: (north_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty V142() V143() V144() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) = a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ;

theorem :: JORDAN18:8
for a being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds upper_bound (proj2 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) V23( REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) Element of bool [: the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .: (south_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty V142() V143() V144() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) = a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ;

theorem :: JORDAN18:9
for a being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds upper_bound (proj1 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) V23( REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) Element of bool [: the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .: (west_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty V142() V143() V144() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) = a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ;

theorem :: JORDAN18:10
for a being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds lower_bound (proj1 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) V23( REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) Element of bool [: the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .: (east_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty V142() V143() V144() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) = a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ;

registration
let a be ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ;
cluster north_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) -> closed ;
cluster south_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) -> closed ;
cluster east_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) -> closed ;
cluster west_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) -> closed ;
end;

theorem :: JORDAN18:11
for P being ( ( ) ( ) Subset of )
for a being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in BDD P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) holds
not north_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty closed ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) c= UBD P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) ;

theorem :: JORDAN18:12
for P being ( ( ) ( ) Subset of )
for a being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in BDD P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) holds
not south_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty closed ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) c= UBD P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) ;

theorem :: JORDAN18:13
for P being ( ( ) ( ) Subset of )
for a being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in BDD P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) holds
not east_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty closed ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) c= UBD P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) ;

theorem :: JORDAN18:14
for P being ( ( ) ( ) Subset of )
for a being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in BDD P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) holds
not west_halfline a : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty closed ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) c= UBD P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) ;

theorem :: JORDAN18:15
for C being ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve)
for P being ( ( ) ( ) Subset of )
for p1, p2 being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) st P : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) & P : ( ( ) ( ) Subset of ) c= C : ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve) holds
ex R being ( ( non empty ) ( non empty ) Subset of ) st
( R : ( ( non empty ) ( non empty ) Subset of ) is_an_arc_of p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) & P : ( ( ) ( ) Subset of ) \/ R : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( non empty ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) = C : ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve) & P : ( ( ) ( ) Subset of ) /\ R : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) = {p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) } : ( ( ) ( non empty ) set ) ) ;

begin

definition
let p be ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ;
let P be ( ( ) ( ) Subset of ) ;
func North-Bound (p,P) -> ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) equals :: JORDAN18:def 1
|[(p : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) `1) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ,(lower_bound (proj2 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) V23( REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) Element of bool [: the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .: (P : ( ( ) ( ) set ) /\ (north_halfline p : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V142() V143() V144() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ;
func South-Bound (p,P) -> ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) equals :: JORDAN18:def 2
|[(p : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) `1) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ,(upper_bound (proj2 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) V23( REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) Element of bool [: the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .: (P : ( ( ) ( ) set ) /\ (south_halfline p : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V142() V143() V144() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ;
end;

theorem :: JORDAN18:16
for P being ( ( ) ( ) Subset of )
for p being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds
( (North-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,P : ( ( ) ( ) Subset of ) )) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) = p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) & (South-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,P : ( ( ) ( ) Subset of ) )) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) = p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ;

theorem :: JORDAN18:17
for p being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) )
for C being ( ( compact ) ( closed compact bounded ) Subset of ) st p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( open ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) holds
( North-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in C : ( ( compact ) ( closed compact bounded ) Subset of ) & North-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in north_halfline p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty closed ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) & South-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in C : ( ( compact ) ( closed compact bounded ) Subset of ) & South-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in south_halfline p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty closed ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: JORDAN18:18
for p being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) )
for C being ( ( compact ) ( closed compact bounded ) Subset of ) st p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( open ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) holds
( (South-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( compact ) ( closed compact bounded ) Subset of ) )) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) < p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) < (North-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( compact ) ( closed compact bounded ) Subset of ) )) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ;

theorem :: JORDAN18:19
for p being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) )
for C being ( ( compact ) ( closed compact bounded ) Subset of ) st p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( open ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) holds
lower_bound (proj2 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) V23( REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) Element of bool [: the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .: (C : ( ( compact ) ( closed compact bounded ) Subset of ) /\ (north_halfline p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty closed ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V142() V143() V144() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) > upper_bound (proj2 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) ( V19() V22( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) V23( REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) , REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ) Element of bool [: the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ,REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .: (C : ( ( compact ) ( closed compact bounded ) Subset of ) /\ (south_halfline p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty closed ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V142() V143() V144() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) ;

theorem :: JORDAN18:20
for p being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) )
for C being ( ( compact ) ( closed compact bounded ) Subset of ) st p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( open ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) holds
South-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) <> North-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ;

theorem :: JORDAN18:21
for p being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) )
for C being ( ( ) ( ) Subset of ) holds LSeg ((North-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( ) ( ) Subset of ) )) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,(South-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( ) ( ) Subset of ) )) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) is vertical ;

theorem :: JORDAN18:22
for p being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) )
for C being ( ( compact ) ( closed compact bounded ) Subset of ) st p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( open ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) holds
(LSeg ((North-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( compact ) ( closed compact bounded ) Subset of ) )) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,(South-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( compact ) ( closed compact bounded ) Subset of ) )) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) )) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) /\ C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) = {(North-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( compact ) ( closed compact bounded ) Subset of ) )) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,(South-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( compact ) ( closed compact bounded ) Subset of ) )) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) } : ( ( ) ( non empty ) set ) ;

theorem :: JORDAN18:23
for p, q being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) )
for C being ( ( compact ) ( closed compact bounded ) Subset of ) st p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( open ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) & q : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in BDD C : ( ( compact ) ( closed compact bounded ) Subset of ) : ( ( ) ( open ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) : ( ( ) ( ) set ) ) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) <> q : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ) holds
North-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) , South-Bound (q : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) , North-Bound (q : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) , South-Bound (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) are_mutually_different ;

begin

definition
let n be ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ;
let V be ( ( ) ( ) Subset of ) ;
let s1, s2, t1, t2 be ( ( ) ( V43(n : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ;
pred s1,s2,V -separate t1,t2 means :: JORDAN18:def 3
 for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is_an_arc_of s1 : ( ( Function-like V33([:n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) ) ( V19() V22([:n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ) V23(n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) Function-like V33([:n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) ) Element of bool [:[:n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,s2 : ( ( Function-like V33([:REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) ) ( V19() V22([:REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ) V23(n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) Function-like V33([:REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) & A : ( ( ) ( ) Subset of ) c= V : ( ( ) ( ) set ) holds
A : ( ( ) ( ) Subset of ) meets {t1 : ( ( ) ( ) Element of bool (bool n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,t2 : ( ( ) ( V19() V22(s1 : ( ( Function-like V33([:n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) ) ( V19() V22([:n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ) V23(n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) Function-like V33([:n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) ) Element of bool [:[:n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) V23(s2 : ( ( Function-like V33([:REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) ) ( V19() V22([:REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ) V23(n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) Function-like V33([:REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) Element of bool [:s1 : ( ( Function-like V33([:n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) ) ( V19() V22([:n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ) V23(n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) Function-like V33([:n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) ) Element of bool [:[:n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,s2 : ( ( Function-like V33([:REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) ) ( V19() V22([:REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ) V23(n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) Function-like V33([:REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) ,n : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty ) set ) ;
end;

notation
let n be ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ;
let V be ( ( ) ( ) Subset of ) ;
let s1, s2, t1, t2 be ( ( ) ( V43(n : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ;
antonym s1,s2 are_neighbours_wrt t1,t2,V for s1,s2,V -separate t1,t2;
end;

theorem :: JORDAN18:24
for n being ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) )
for V being ( ( ) ( ) Subset of )
for t, s1, s2 being ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds t : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,t : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,V : ( ( ) ( ) Subset of ) -separate s1 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,s2 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ;

theorem :: JORDAN18:25
for n being ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) )
for V being ( ( ) ( ) Subset of )
for s1, s2, t1, t2 being ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) st s1 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,s2 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,V : ( ( ) ( ) Subset of ) -separate t1 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,t2 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds
s2 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,s1 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,V : ( ( ) ( ) Subset of ) -separate t1 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,t2 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ;

theorem :: JORDAN18:26
for n being ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) )
for V being ( ( ) ( ) Subset of )
for s1, s2, t1, t2 being ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) st s1 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,s2 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,V : ( ( ) ( ) Subset of ) -separate t1 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,t2 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds
s1 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,s2 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,V : ( ( ) ( ) Subset of ) -separate t2 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,t1 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ;

theorem :: JORDAN18:27
for n being ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) )
for V being ( ( ) ( ) Subset of )
for s, t1, t2 being ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds s : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,t1 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,V : ( ( ) ( ) Subset of ) -separate s : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,t2 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ;

theorem :: JORDAN18:28
for n being ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) )
for V being ( ( ) ( ) Subset of )
for t1, s, t2 being ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds t1 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,s : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,V : ( ( ) ( ) Subset of ) -separate t2 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,s : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ;

theorem :: JORDAN18:29
for n being ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) )
for V being ( ( ) ( ) Subset of )
for t1, s, t2 being ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds t1 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,s : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,V : ( ( ) ( ) Subset of ) -separate s : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,t2 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ;

theorem :: JORDAN18:30
for n being ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) )
for V being ( ( ) ( ) Subset of )
for s, t1, t2 being ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds s : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,t1 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,V : ( ( ) ( ) Subset of ) -separate t2 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,s : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ;

theorem :: JORDAN18:31
for C being ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve)
for p1, p2, q being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) st q : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in C : ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve) & p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in C : ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve) & p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in C : ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve) & p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) <> p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) & p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) <> q : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) & p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) <> q : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds
p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) are_neighbours_wrt q : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,q : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve) ;

theorem :: JORDAN18:32
for C being ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve)
for p1, p2, q1, q2 being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) st p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) <> p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) & p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in C : ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve) & p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in C : ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve) & p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve) -separate q1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,q2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) holds
q1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,q2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve) -separate p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ;

theorem :: JORDAN18:33
for C being ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve)
for p1, p2, q1, q2 being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) st p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in C : ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve) & p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in C : ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve) & q1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) in C : ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve) & p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) <> p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) & q1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) <> p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) & q1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) <> p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) & q2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) <> p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) & q2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) <> p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) & not p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) are_neighbours_wrt q1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,q2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve) holds
p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,q1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) are_neighbours_wrt p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,q2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() ) Element of NAT : ( ( ) ( V142() V143() V144() V145() V146() V147() V148() ) Element of bool REAL : ( ( ) ( non empty V36() V142() V143() V144() V148() ) set ) : ( ( ) ( ) set ) ) ) ) V76() V134() ) Point of ( ( ) ( non empty functional ) set ) ) ,C : ( ( being_simple_closed_curve ) ( being_simple_closed_curve ) Simple_closed_curve) ;