:: JORDAN5A semantic presentation

begin

theorem :: JORDAN5A:1
for n being ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) )
for p, q being ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) )
for P being ( ( ) ( functional ) Subset of ) st P : ( ( ) ( functional ) Subset of ) is_an_arc_of p : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ,q : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) holds
P : ( ( ) ( functional ) Subset of ) is compact ;

theorem :: JORDAN5A:2
for n being ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) )
for p1, p2 being ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) )
for r1, r2 being ( ( real ) ( V11() real ext-real ) number ) holds
( not ((1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) - r1 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) * p1 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Element of the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) + (r1 : ( ( real ) ( V11() real ext-real ) number ) * p2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Element of the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Element of the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) = ((1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) - r2 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) * p1 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Element of the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) + (r2 : ( ( real ) ( V11() real ext-real ) number ) * p2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Element of the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Element of the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) or r1 : ( ( real ) ( V11() real ext-real ) number ) = r2 : ( ( real ) ( V11() real ext-real ) number ) or p1 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) = p2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ) ;

theorem :: JORDAN5A:3
for n being ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) )
for p1, p2 being ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) st p1 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) <> p2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) holds
ex f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) | (LSeg (b2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ,b3 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) )) : ( ( ) ( non empty functional V231( TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) ) ) Element of K6( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty ) set ) ) st
( ( for x being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Real) in [.0 : ( ( ) ( empty natural V11() real ext-real non positive non negative Function-like functional V43() V44() V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) .] : ( ( ) ( V45() V46() V47() V66() closed ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) holds
f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) | (LSeg (b2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ,b3 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) )) : ( ( ) ( non empty functional V231( TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) ) ) Element of K6( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( ) set ) = ((1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) - x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) * p1 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Element of the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) + (x : ( ( ) ( V11() real ext-real ) Real) * p2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Element of the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Element of the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) | (LSeg (b2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ,b3 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) )) : ( ( ) ( non empty functional V231( TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) ) ) Element of K6( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) | (LSeg (b2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ,b3 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) )) : ( ( ) ( non empty functional V231( TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) ) ) Element of K6( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty ) set ) ) . 0 : ( ( ) ( empty natural V11() real ext-real non positive non negative Function-like functional V43() V44() V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = p1 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) | (LSeg (b2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ,b3 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) )) : ( ( ) ( non empty functional V231( TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) ) ) Element of K6( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty ) set ) ) . 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = p2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(b1 : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ) ;

registration
let n be ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;
cluster TOP-REAL n : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict ) RLTopStruct ) -> strict pathwise_connected ;
end;

registration
let n be ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;
cluster non empty strict TopSpace-like T_0 T_1 T_2 compact for ( ( ) ( ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) ;
end;

theorem :: JORDAN5A:4
for a, b being ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) )
for f being ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) -valued Function-like total quasi_total continuous ) Path of a : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ,b : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) )
for P being ( ( non empty compact ) ( non empty TopSpace-like T_0 T_1 T_2 compact pseudocompact ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) )
for g being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of b4 : ( ( non empty compact ) ( non empty TopSpace-like T_0 T_1 T_2 compact pseudocompact ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) -valued Function-like total quasi_total continuous ) Path of b1 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ,b2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ) is one-to-one & g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of b4 : ( ( non empty compact ) ( non empty TopSpace-like T_0 T_1 T_2 compact pseudocompact ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty ) set ) ) = f : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) -valued Function-like total quasi_total continuous ) Path of b1 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ,b2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ) & [#] P : ( ( non empty compact ) ( non empty TopSpace-like T_0 T_1 T_2 compact pseudocompact ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( non empty non proper open closed dense non boundary ) Element of K6( the carrier of b4 : ( ( non empty compact ) ( non empty TopSpace-like T_0 T_1 T_2 compact pseudocompact ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = rng f : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) -valued Function-like total quasi_total continuous ) Path of b1 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ,b2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( functional ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty ) set ) ) holds
g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of b4 : ( ( non empty compact ) ( non empty TopSpace-like T_0 T_1 T_2 compact pseudocompact ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism ;

begin

theorem :: JORDAN5A:5
for X being ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) holds
( X : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) in Family_open_set RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V129() triangle Discerning V212() ) MetrStruct ) : ( ( ) ( ) Element of K6(K6( the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V129() triangle Discerning V212() ) MetrStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) iff X : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) is open ) ;

theorem :: JORDAN5A:6
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) )
for x being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) )
for g being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -defined REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,)
for x1 being ( ( ) ( V11() real ext-real ) Real) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is_continuous_at x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) = g : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -defined REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) & x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) = x1 : ( ( ) ( V11() real ext-real ) Real) holds
g : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -defined REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) is_continuous_in x1 : ( ( ) ( V11() real ext-real ) Real) ;

theorem :: JORDAN5A:7
for f being ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) )
for g being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -defined REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) st f : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) = g : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -defined REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) holds
g : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -defined REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) is continuous ;

theorem :: JORDAN5A:8
for f being ( ( Function-like one-to-one quasi_total continuous ) ( non empty Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like one-to-one total quasi_total V33() V34() V35() continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) holds
( for x, y being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) )
for p, q, fx, fy being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) = p : ( ( ) ( V11() real ext-real ) Real) & y : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) = q : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V11() real ext-real ) Real) < q : ( ( ) ( V11() real ext-real ) Real) & fx : ( ( ) ( V11() real ext-real ) Real) = f : ( ( Function-like one-to-one quasi_total continuous ) ( non empty Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like one-to-one total quasi_total V33() V34() V35() continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) set ) & fy : ( ( ) ( V11() real ext-real ) Real) = f : ( ( Function-like one-to-one quasi_total continuous ) ( non empty Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like one-to-one total quasi_total V33() V34() V35() continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . y : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) set ) holds
fx : ( ( ) ( V11() real ext-real ) Real) < fy : ( ( ) ( V11() real ext-real ) Real) or for x, y being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) )
for p, q, fx, fy being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) = p : ( ( ) ( V11() real ext-real ) Real) & y : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) = q : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V11() real ext-real ) Real) < q : ( ( ) ( V11() real ext-real ) Real) & fx : ( ( ) ( V11() real ext-real ) Real) = f : ( ( Function-like one-to-one quasi_total continuous ) ( non empty Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like one-to-one total quasi_total V33() V34() V35() continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) set ) & fy : ( ( ) ( V11() real ext-real ) Real) = f : ( ( Function-like one-to-one quasi_total continuous ) ( non empty Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like one-to-one total quasi_total V33() V34() V35() continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . y : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) set ) holds
fx : ( ( ) ( V11() real ext-real ) Real) > fy : ( ( ) ( V11() real ext-real ) Real) ) ;

theorem :: JORDAN5A:9
for r, gg, a, b being ( ( ) ( V11() real ext-real ) Real)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( V11() real ext-real ) Real) <= b : ( ( ) ( V11() real ext-real ) Real) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = r : ( ( ) ( V11() real ext-real ) Real) & ].(r : ( ( ) ( V11() real ext-real ) Real) - gg : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) ,(r : ( ( ) ( V11() real ext-real ) Real) + gg : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) .[ : ( ( ) ( V45() V46() V47() non left_end non right_end V66() open ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) c= [.a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V66() closed ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) holds
].(r : ( ( ) ( V11() real ext-real ) Real) - gg : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) ,(r : ( ( ) ( V11() real ext-real ) Real) + gg : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) .[ : ( ( ) ( V45() V46() V47() non left_end non right_end V66() open ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) = Ball (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,gg : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( ) Element of K6( the carrier of (Closed-Interval-MSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V129() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V129() triangle Discerning V212() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: JORDAN5A:10
for a, b being ( ( ) ( V11() real ext-real ) Real)
for X being ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( V11() real ext-real ) Real) < b : ( ( ) ( V11() real ext-real ) Real) & not a : ( ( ) ( V11() real ext-real ) Real) in X : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) & not b : ( ( ) ( V11() real ext-real ) Real) in X : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) & X : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) in Family_open_set (Closed-Interval-MSpace (a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V129() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V129() triangle Discerning V212() ) MetrStruct ) ) : ( ( ) ( ) Element of K6(K6( the carrier of (Closed-Interval-MSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V129() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V129() triangle Discerning V212() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
X : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) is open ;

theorem :: JORDAN5A:11
for X being ( ( open ) ( V45() V46() V47() open ) Subset of ( ( ) ( non empty ) set ) )
for a, b being ( ( ) ( V11() real ext-real ) Real) st X : ( ( open ) ( V45() V46() V47() open ) Subset of ( ( ) ( non empty ) set ) ) c= [.a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V66() closed ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) holds
( not a : ( ( ) ( V11() real ext-real ) Real) in X : ( ( open ) ( V45() V46() V47() open ) Subset of ( ( ) ( non empty ) set ) ) & not b : ( ( ) ( V11() real ext-real ) Real) in X : ( ( open ) ( V45() V46() V47() open ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: JORDAN5A:12
for a, b being ( ( ) ( V11() real ext-real ) Real)
for X being ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) )
for V being ( ( ) ( ) Subset of ) st V : ( ( ) ( ) Subset of ) = X : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) & X : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) is open holds
V : ( ( ) ( ) Subset of ) in Family_open_set (Closed-Interval-MSpace (a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V129() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V129() triangle Discerning V212() ) MetrStruct ) ) : ( ( ) ( ) Element of K6(K6( the carrier of (Closed-Interval-MSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict Reflexive discerning V129() triangle Discerning ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V129() triangle Discerning V212() ) MetrStruct ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: JORDAN5A:13
for a, b, c, d, x1 being ( ( ) ( V11() real ext-real ) Real)
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) )
for x being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) )
for g being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -defined REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) st a : ( ( ) ( V11() real ext-real ) Real) < b : ( ( ) ( V11() real ext-real ) Real) & c : ( ( ) ( V11() real ext-real ) Real) < d : ( ( ) ( V11() real ext-real ) Real) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is_continuous_at x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . a : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) set ) = c : ( ( ) ( V11() real ext-real ) Real) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . b : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) set ) = d : ( ( ) ( V11() real ext-real ) Real) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is one-to-one & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) = g : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -defined REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) & x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) = x1 : ( ( ) ( V11() real ext-real ) Real) holds
g : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -defined REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) | [.a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V66() closed ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -defined REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -valued Function-like V33() V34() V35() ) Element of K6(K7(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ,REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty V33() V34() V35() ) set ) ) : ( ( ) ( non empty ) set ) ) is_continuous_in x1 : ( ( ) ( V11() real ext-real ) Real) ;

theorem :: JORDAN5A:14
for a, b, c, d being ( ( ) ( V11() real ext-real ) Real)
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) )
for g being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -defined REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is continuous & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is one-to-one & a : ( ( ) ( V11() real ext-real ) Real) < b : ( ( ) ( V11() real ext-real ) Real) & c : ( ( ) ( V11() real ext-real ) Real) < d : ( ( ) ( V11() real ext-real ) Real) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) = g : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -defined REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . a : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) set ) = c : ( ( ) ( V11() real ext-real ) Real) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . b : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) set ) = d : ( ( ) ( V11() real ext-real ) Real) holds
g : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -defined REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) | [.a : ( ( ) ( V11() real ext-real ) Real) ,b : ( ( ) ( V11() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V66() closed ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -defined REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -valued Function-like V33() V34() V35() ) Element of K6(K7(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ,REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty V33() V34() V35() ) set ) ) : ( ( ) ( non empty ) set ) ) is continuous ;

begin

theorem :: JORDAN5A:15
for a, b, c, d being ( ( ) ( V11() real ext-real ) Real)
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) st a : ( ( ) ( V11() real ext-real ) Real) < b : ( ( ) ( V11() real ext-real ) Real) & c : ( ( ) ( V11() real ext-real ) Real) < d : ( ( ) ( V11() real ext-real ) Real) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is continuous & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is one-to-one & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . a : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) set ) = c : ( ( ) ( V11() real ext-real ) Real) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . b : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) set ) = d : ( ( ) ( V11() real ext-real ) Real) holds
for x, y being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) )
for p, q, fx, fy being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) = p : ( ( ) ( V11() real ext-real ) Real) & y : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) = q : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V11() real ext-real ) Real) < q : ( ( ) ( V11() real ext-real ) Real) & fx : ( ( ) ( V11() real ext-real ) Real) = f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) & fy : ( ( ) ( V11() real ext-real ) Real) = f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . y : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) holds
fx : ( ( ) ( V11() real ext-real ) Real) < fy : ( ( ) ( V11() real ext-real ) Real) ;

theorem :: JORDAN5A:16
for f being ( ( Function-like one-to-one quasi_total continuous ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like one-to-one total quasi_total V33() V34() V35() continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) st f : ( ( Function-like one-to-one quasi_total continuous ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like one-to-one total quasi_total V33() V34() V35() continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . 0 : ( ( ) ( empty natural V11() real ext-real non positive non negative Function-like functional V43() V44() V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) = 0 : ( ( ) ( empty natural V11() real ext-real non positive non negative Function-like functional V43() V44() V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) & f : ( ( Function-like one-to-one quasi_total continuous ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like one-to-one total quasi_total V33() V34() V35() continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) = 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
for x, y being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) )
for p, q, fx, fy being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) = p : ( ( ) ( V11() real ext-real ) Real) & y : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) = q : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V11() real ext-real ) Real) < q : ( ( ) ( V11() real ext-real ) Real) & fx : ( ( ) ( V11() real ext-real ) Real) = f : ( ( Function-like one-to-one quasi_total continuous ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like one-to-one total quasi_total V33() V34() V35() continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) & fy : ( ( ) ( V11() real ext-real ) Real) = f : ( ( Function-like one-to-one quasi_total continuous ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like one-to-one total quasi_total V33() V34() V35() continuous ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . y : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) holds
fx : ( ( ) ( V11() real ext-real ) Real) < fy : ( ( ) ( V11() real ext-real ) Real) ;

theorem :: JORDAN5A:17
for a, b, c, d being ( ( ) ( V11() real ext-real ) Real)
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) )
for P being ( ( non empty ) ( non empty V45() V46() V47() ) Subset of )
for PP, QQ being ( ( ) ( V45() V46() V47() ) Subset of ) st a : ( ( ) ( V11() real ext-real ) Real) < b : ( ( ) ( V11() real ext-real ) Real) & c : ( ( ) ( V11() real ext-real ) Real) < d : ( ( ) ( V11() real ext-real ) Real) & PP : ( ( ) ( V45() V46() V47() ) Subset of ) = P : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is continuous & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is one-to-one & PP : ( ( ) ( V45() V46() V47() ) Subset of ) is compact & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . a : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) set ) = c : ( ( ) ( V11() real ext-real ) Real) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . b : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) set ) = d : ( ( ) ( V11() real ext-real ) Real) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) .: P : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ) : ( ( ) ( V45() V46() V47() ) Element of K6( the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( non empty ) set ) ) = QQ : ( ( ) ( V45() V46() V47() ) Subset of ) holds
f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . (lower_bound ([#] PP : ( ( ) ( V45() V46() V47() ) Subset of ) ) : ( ( ) ( V45() V46() V47() ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( V11() real ext-real ) set ) = lower_bound ([#] QQ : ( ( ) ( V45() V46() V47() ) Subset of ) ) : ( ( ) ( V45() V46() V47() ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) ;

theorem :: JORDAN5A:18
for a, b, c, d being ( ( ) ( V11() real ext-real ) Real)
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) )
for P, Q being ( ( non empty ) ( non empty V45() V46() V47() ) Subset of )
for PP, QQ being ( ( ) ( V45() V46() V47() ) Subset of ) st a : ( ( ) ( V11() real ext-real ) Real) < b : ( ( ) ( V11() real ext-real ) Real) & c : ( ( ) ( V11() real ext-real ) Real) < d : ( ( ) ( V11() real ext-real ) Real) & PP : ( ( ) ( V45() V46() V47() ) Subset of ) = P : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ) & QQ : ( ( ) ( V45() V46() V47() ) Subset of ) = Q : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is continuous & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is one-to-one & PP : ( ( ) ( V45() V46() V47() ) Subset of ) is compact & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . a : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) set ) = c : ( ( ) ( V11() real ext-real ) Real) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . b : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) set ) = d : ( ( ) ( V11() real ext-real ) Real) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) .: P : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ) : ( ( ) ( V45() V46() V47() ) Element of K6( the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( non empty ) set ) ) = Q : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ) holds
f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . (upper_bound ([#] PP : ( ( ) ( V45() V46() V47() ) Subset of ) ) : ( ( ) ( V45() V46() V47() ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( V11() real ext-real ) set ) = upper_bound ([#] QQ : ( ( ) ( V45() V46() V47() ) Subset of ) ) : ( ( ) ( V45() V46() V47() ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) ;

theorem :: JORDAN5A:19
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) holds
( lower_bound [.a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) .] : ( ( ) ( V45() V46() V47() V66() closed ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) = a : ( ( real ) ( V11() real ext-real ) number ) & upper_bound [.a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) .] : ( ( ) ( V45() V46() V47() V66() closed ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) = b : ( ( real ) ( V11() real ext-real ) number ) ) ;

theorem :: JORDAN5A:20
for a, b, c, d, e, f, g, h being ( ( ) ( V11() real ext-real ) Real)
for F being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) st a : ( ( ) ( V11() real ext-real ) Real) < b : ( ( ) ( V11() real ext-real ) Real) & c : ( ( ) ( V11() real ext-real ) Real) < d : ( ( ) ( V11() real ext-real ) Real) & e : ( ( ) ( V11() real ext-real ) Real) < f : ( ( ) ( V11() real ext-real ) Real) & a : ( ( ) ( V11() real ext-real ) Real) <= e : ( ( ) ( V11() real ext-real ) Real) & f : ( ( ) ( V11() real ext-real ) Real) <= b : ( ( ) ( V11() real ext-real ) Real) & F : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is being_homeomorphism & F : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . a : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) set ) = c : ( ( ) ( V11() real ext-real ) Real) & F : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . b : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) set ) = d : ( ( ) ( V11() real ext-real ) Real) & g : ( ( ) ( V11() real ext-real ) Real) = F : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . e : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) set ) & h : ( ( ) ( V11() real ext-real ) Real) = F : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) . f : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) set ) holds
F : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b1 : ( ( ) ( V11() real ext-real ) Real) ,b2 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) .: [.e : ( ( ) ( V11() real ext-real ) Real) ,f : ( ( ) ( V11() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V66() closed ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of K6( the carrier of (Closed-Interval-TSpace (b3 : ( ( ) ( V11() real ext-real ) Real) ,b4 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V212() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( non empty ) set ) ) = [.g : ( ( ) ( V11() real ext-real ) Real) ,h : ( ( ) ( V11() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V66() closed ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: JORDAN5A:21
for P, Q being ( ( ) ( functional ) Subset of )
for p1, p2 being ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) st P : ( ( ) ( functional ) Subset of ) meets Q : ( ( ) ( functional ) Subset of ) & P : ( ( ) ( functional ) Subset of ) /\ Q : ( ( ) ( functional ) Subset of ) : ( ( ) ( functional ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty ) set ) ) is closed & P : ( ( ) ( functional ) Subset of ) is_an_arc_of p1 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ,p2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) holds
ex EX being ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) st
( EX : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) in P : ( ( ) ( functional ) Subset of ) /\ Q : ( ( ) ( functional ) Subset of ) : ( ( ) ( functional ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty ) set ) ) & ex g being ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) | b1 : ( ( ) ( functional ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( ) set ) ) ex s2 being ( ( ) ( V11() real ext-real ) Real) st
( g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) | b1 : ( ( ) ( functional ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( ) set ) ) is being_homeomorphism & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) | b1 : ( ( ) ( functional ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( ) set ) ) . 0 : ( ( ) ( empty natural V11() real ext-real non positive non negative Function-like functional V43() V44() V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = p1 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) | b1 : ( ( ) ( functional ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( ) set ) ) . 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = p2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) | b1 : ( ( ) ( functional ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( ) set ) ) . s2 : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( ) set ) = EX : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) & 0 : ( ( ) ( empty natural V11() real ext-real non positive non negative Function-like functional V43() V44() V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & s2 : ( ( ) ( V11() real ext-real ) Real) <= 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) & ( for t being ( ( ) ( V11() real ext-real ) Real) st 0 : ( ( ) ( empty natural V11() real ext-real non positive non negative Function-like functional V43() V44() V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) <= t : ( ( ) ( V11() real ext-real ) Real) & t : ( ( ) ( V11() real ext-real ) Real) < s2 : ( ( ) ( V11() real ext-real ) Real) holds
not g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) | b1 : ( ( ) ( functional ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( ) set ) ) . t : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( ) set ) in Q : ( ( ) ( functional ) Subset of ) ) ) ) ;

theorem :: JORDAN5A:22
for P, Q being ( ( ) ( functional ) Subset of )
for p1, p2 being ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) st P : ( ( ) ( functional ) Subset of ) meets Q : ( ( ) ( functional ) Subset of ) & P : ( ( ) ( functional ) Subset of ) /\ Q : ( ( ) ( functional ) Subset of ) : ( ( ) ( functional ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty ) set ) ) is closed & P : ( ( ) ( functional ) Subset of ) is_an_arc_of p1 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) ,p2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) holds
ex EX being ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) st
( EX : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) in P : ( ( ) ( functional ) Subset of ) /\ Q : ( ( ) ( functional ) Subset of ) : ( ( ) ( functional ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty ) set ) ) & ex g being ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) | b1 : ( ( ) ( functional ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( ) set ) ) ex s2 being ( ( ) ( V11() real ext-real ) Real) st
( g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) | b1 : ( ( ) ( functional ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( ) set ) ) is being_homeomorphism & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) | b1 : ( ( ) ( functional ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( ) set ) ) . 0 : ( ( ) ( empty natural V11() real ext-real non positive non negative Function-like functional V43() V44() V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = p1 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) | b1 : ( ( ) ( functional ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( ) set ) ) . 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = p2 : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) | b1 : ( ( ) ( functional ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( ) set ) ) . s2 : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( ) set ) = EX : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V70() ) Point of ( ( ) ( non empty functional ) set ) ) & 0 : ( ( ) ( empty natural V11() real ext-real non positive non negative Function-like functional V43() V44() V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & s2 : ( ( ) ( V11() real ext-real ) Real) <= 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) & ( for t being ( ( ) ( V11() real ext-real ) Real) st 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) >= t : ( ( ) ( V11() real ext-real ) Real) & t : ( ( ) ( V11() real ext-real ) Real) > s2 : ( ( ) ( V11() real ext-real ) Real) holds
not g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) ) : ( ( ) ( non empty V45() V46() V47() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) | b1 : ( ( ) ( functional ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V45() V46() V47() ) set ) , ( ( ) ( ) set ) ) . t : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( ) set ) in Q : ( ( ) ( functional ) Subset of ) ) ) ) ;

registration
cluster non empty V45() V46() V47() finite real-bounded for ( ( ) ( ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: JORDAN5A:23
for A being ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) )
for B being ( ( ) ( V45() V46() V47() ) Subset of ) st A : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) = B : ( ( ) ( V45() V46() V47() ) Subset of ) holds
( A : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) is closed iff B : ( ( ) ( V45() V46() V47() ) Subset of ) is closed ) ;

theorem :: JORDAN5A:24
for A being ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) )
for B being ( ( ) ( V45() V46() V47() ) Subset of ) st A : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) = B : ( ( ) ( V45() V46() V47() ) Subset of ) holds
Cl A : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) = Cl B : ( ( ) ( V45() V46() V47() ) Subset of ) : ( ( ) ( V45() V46() V47() closed ) Element of K6( the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

registration
let a, b be ( ( real ) ( V11() real ext-real ) number ) ;
cluster K289(a : ( ( real ) ( V11() real ext-real ) set ) ,b : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V66() ) set ) -> compact for ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) ;
end;

theorem :: JORDAN5A:25
for A being ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) )
for B being ( ( ) ( V45() V46() V47() ) Subset of ) st A : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) = B : ( ( ) ( V45() V46() V47() ) Subset of ) holds
( A : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( non empty ) set ) ) is compact iff B : ( ( ) ( V45() V46() V47() ) Subset of ) is compact ) ;

registration
cluster finite -> compact for ( ( ) ( ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: JORDAN5A:26
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 ) iff Cl ].a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) .[ : ( ( ) ( V45() V46() V47() non left_end non right_end V66() open ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) = [.a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) .] : ( ( ) ( V45() V46() V47() V66() compact closed ) Element of K6(REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: JORDAN5A:27
for T being ( ( ) ( ) TopStruct )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) RealMap of ( ( ) ( ) set ) )
for g being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) RealMap of ( ( ) ( ) set ) ) = g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) holds
( f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) RealMap of ( ( ) ( ) set ) ) is continuous iff g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V212() ) TopStruct ) : ( ( ) ( non empty V45() V46() V47() ) set ) -valued Function-like total quasi_total V33() V34() V35() ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty V45() V46() V47() ) set ) ) is continuous ) ;