:: JORDAN1 semantic presentation

begin

theorem :: JORDAN1:1
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st ( for x, y being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ex h being ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st
( h : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous & x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = h : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . 0 : ( ( ) ( empty natural V11() real ext-real V115() V116() V163() V164() V165() V166() V167() V168() V169() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) & y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = h : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . 1 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) ) holds
GX : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is connected ;

theorem :: JORDAN1:2
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) st ( for xa, ya being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st xa : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) & ya : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) & xa : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) <> ya : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
ex h being ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V26( the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) st
( h : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V26( the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) is continuous & xa : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = h : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V26( the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) . 0 : ( ( ) ( empty natural V11() real ext-real V115() V116() V163() V164() V165() V166() V167() V168() V169() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) & ya : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = h : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V26( the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) . 1 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) ) holds
A : ( ( ) ( ) Subset of ) is connected ;

theorem :: JORDAN1:3
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A0, A1 being ( ( ) ( ) Subset of ) st A0 : ( ( ) ( ) Subset of ) is connected & A1 : ( ( ) ( ) Subset of ) is connected & A0 : ( ( ) ( ) Subset of ) meets A1 : ( ( ) ( ) Subset of ) holds
A0 : ( ( ) ( ) Subset of ) \/ A1 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is connected ;

theorem :: JORDAN1:4
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A0, A1, A2 being ( ( ) ( ) Subset of ) st A0 : ( ( ) ( ) Subset of ) is connected & A1 : ( ( ) ( ) Subset of ) is connected & A2 : ( ( ) ( ) Subset of ) is connected & A0 : ( ( ) ( ) Subset of ) meets A1 : ( ( ) ( ) Subset of ) & A1 : ( ( ) ( ) Subset of ) meets A2 : ( ( ) ( ) Subset of ) holds
(A0 : ( ( ) ( ) Subset of ) \/ A1 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \/ A2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is connected ;

theorem :: JORDAN1:5
for GX being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A0, A1, A2, A3 being ( ( ) ( ) Subset of ) st A0 : ( ( ) ( ) Subset of ) is connected & A1 : ( ( ) ( ) Subset of ) is connected & A2 : ( ( ) ( ) Subset of ) is connected & A3 : ( ( ) ( ) Subset of ) is connected & A0 : ( ( ) ( ) Subset of ) meets A1 : ( ( ) ( ) Subset of ) & A1 : ( ( ) ( ) Subset of ) meets A2 : ( ( ) ( ) Subset of ) & A2 : ( ( ) ( ) Subset of ) meets A3 : ( ( ) ( ) Subset of ) holds
((A0 : ( ( ) ( ) Subset of ) \/ A1 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \/ A2 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \/ A3 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is connected ;

begin

definition
let V be ( ( non empty V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ;
let P be ( ( ) ( ) Subset of ) ;
redefine attr P is convex means :: JORDAN1:def 1
 for w1, w2 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st w1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) Element of V : ( ( ) ( ) RLTopStruct ) ) & w2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) Element of V : ( ( ) ( ) RLTopStruct ) ) holds
LSeg (w1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of V : ( ( ) ( ) RLTopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) c= P : ( ( ) ( ) Element of V : ( ( ) ( ) RLTopStruct ) ) ;
end;

registration
let n be ( ( natural ) ( natural V11() real ext-real ) Nat) ;
cluster convex -> connected for ( ( ) ( ) Element of K6( the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: JORDAN1:6
canceled;

theorem :: JORDAN1:7
for s1, s2, t1, t2 being ( ( ) ( V11() real ext-real ) Real) holds { |[s : ( ( ) ( V11() real ext-real ) Real) ,t : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s, t is ( ( ) ( V11() real ext-real ) Real) : ( s1 : ( ( ) ( V11() real ext-real ) Real) < s : ( ( ) ( V11() real ext-real ) Real) & s : ( ( ) ( V11() real ext-real ) Real) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < t : ( ( ) ( V11() real ext-real ) Real) & t : ( ( ) ( V11() real ext-real ) Real) < t2 : ( ( ) ( V11() real ext-real ) Real) ) } = (( { |[s3 : ( ( ) ( V11() real ext-real ) Real) ,t3 : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s3, t3 is ( ( ) ( V11() real ext-real ) Real) : s1 : ( ( ) ( V11() real ext-real ) Real) < s3 : ( ( ) ( V11() real ext-real ) Real) } /\ { |[s4 : ( ( ) ( V11() real ext-real ) Real) ,t4 : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s4, t4 is ( ( ) ( V11() real ext-real ) Real) : s4 : ( ( ) ( V11() real ext-real ) Real) < s2 : ( ( ) ( V11() real ext-real ) Real) } ) : ( ( ) ( ) set ) /\ { |[s5 : ( ( ) ( V11() real ext-real ) Real) ,t5 : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s5, t5 is ( ( ) ( V11() real ext-real ) Real) : t1 : ( ( ) ( V11() real ext-real ) Real) < t5 : ( ( ) ( V11() real ext-real ) Real) } ) : ( ( ) ( ) set ) /\ { |[s6 : ( ( ) ( V11() real ext-real ) Real) ,t6 : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s6, t6 is ( ( ) ( V11() real ext-real ) Real) : t6 : ( ( ) ( V11() real ext-real ) Real) < t2 : ( ( ) ( V11() real ext-real ) Real) } : ( ( ) ( ) set ) ;

theorem :: JORDAN1:8
for s1, s2, t1, t2 being ( ( ) ( V11() real ext-real ) Real) holds { |[s : ( ( ) ( V11() real ext-real ) Real) ,t : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s, t is ( ( ) ( V11() real ext-real ) Real) : ( not s1 : ( ( ) ( V11() real ext-real ) Real) <= s : ( ( ) ( V11() real ext-real ) Real) or not s : ( ( ) ( V11() real ext-real ) Real) <= s2 : ( ( ) ( V11() real ext-real ) Real) or not t1 : ( ( ) ( V11() real ext-real ) Real) <= t : ( ( ) ( V11() real ext-real ) Real) or not t : ( ( ) ( V11() real ext-real ) Real) <= t2 : ( ( ) ( V11() real ext-real ) Real) ) } = (( { |[s3 : ( ( ) ( V11() real ext-real ) Real) ,t3 : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s3, t3 is ( ( ) ( V11() real ext-real ) Real) : s3 : ( ( ) ( V11() real ext-real ) Real) < s1 : ( ( ) ( V11() real ext-real ) Real) } \/ { |[s4 : ( ( ) ( V11() real ext-real ) Real) ,t4 : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s4, t4 is ( ( ) ( V11() real ext-real ) Real) : t4 : ( ( ) ( V11() real ext-real ) Real) < t1 : ( ( ) ( V11() real ext-real ) Real) } ) : ( ( ) ( ) set ) \/ { |[s5 : ( ( ) ( V11() real ext-real ) Real) ,t5 : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s5, t5 is ( ( ) ( V11() real ext-real ) Real) : s2 : ( ( ) ( V11() real ext-real ) Real) < s5 : ( ( ) ( V11() real ext-real ) Real) } ) : ( ( ) ( ) set ) \/ { |[s6 : ( ( ) ( V11() real ext-real ) Real) ,t6 : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s6, t6 is ( ( ) ( V11() real ext-real ) Real) : t2 : ( ( ) ( V11() real ext-real ) Real) < t6 : ( ( ) ( V11() real ext-real ) Real) } : ( ( ) ( ) set ) ;

theorem :: JORDAN1:9
for s1, t1, s2, t2 being ( ( ) ( V11() real ext-real ) Real)
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { |[s : ( ( ) ( V11() real ext-real ) Real) ,t : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s, t is ( ( ) ( V11() real ext-real ) Real) : ( s1 : ( ( ) ( V11() real ext-real ) Real) < s : ( ( ) ( V11() real ext-real ) Real) & s : ( ( ) ( V11() real ext-real ) Real) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < t : ( ( ) ( V11() real ext-real ) Real) & t : ( ( ) ( V11() real ext-real ) Real) < t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
P : ( ( ) ( ) Subset of ) is convex ;

theorem :: JORDAN1:10
canceled;

theorem :: JORDAN1:11
for s1 being ( ( ) ( V11() real ext-real ) Real)
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { |[s : ( ( ) ( V11() real ext-real ) Real) ,t : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s, t is ( ( ) ( V11() real ext-real ) Real) : s1 : ( ( ) ( V11() real ext-real ) Real) < s : ( ( ) ( V11() real ext-real ) Real) } holds
P : ( ( ) ( ) Subset of ) is convex ;

theorem :: JORDAN1:12
canceled;

theorem :: JORDAN1:13
for s2 being ( ( ) ( V11() real ext-real ) Real)
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { |[s : ( ( ) ( V11() real ext-real ) Real) ,t : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s, t is ( ( ) ( V11() real ext-real ) Real) : s : ( ( ) ( V11() real ext-real ) Real) < s2 : ( ( ) ( V11() real ext-real ) Real) } holds
P : ( ( ) ( ) Subset of ) is convex ;

theorem :: JORDAN1:14
canceled;

theorem :: JORDAN1:15
for t1 being ( ( ) ( V11() real ext-real ) Real)
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { |[s : ( ( ) ( V11() real ext-real ) Real) ,t : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s, t is ( ( ) ( V11() real ext-real ) Real) : t1 : ( ( ) ( V11() real ext-real ) Real) < t : ( ( ) ( V11() real ext-real ) Real) } holds
P : ( ( ) ( ) Subset of ) is convex ;

theorem :: JORDAN1:16
canceled;

theorem :: JORDAN1:17
for t2 being ( ( ) ( V11() real ext-real ) Real)
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { |[s : ( ( ) ( V11() real ext-real ) Real) ,t : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s, t is ( ( ) ( V11() real ext-real ) Real) : t : ( ( ) ( V11() real ext-real ) Real) < t2 : ( ( ) ( V11() real ext-real ) Real) } holds
P : ( ( ) ( ) Subset of ) is convex ;

theorem :: JORDAN1:18
canceled;

theorem :: JORDAN1:19
for s1, t1, s2, t2 being ( ( ) ( V11() real ext-real ) Real)
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { |[s : ( ( ) ( V11() real ext-real ) Real) ,t : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s, t is ( ( ) ( V11() real ext-real ) Real) : ( not s1 : ( ( ) ( V11() real ext-real ) Real) <= s : ( ( ) ( V11() real ext-real ) Real) or not s : ( ( ) ( V11() real ext-real ) Real) <= s2 : ( ( ) ( V11() real ext-real ) Real) or not t1 : ( ( ) ( V11() real ext-real ) Real) <= t : ( ( ) ( V11() real ext-real ) Real) or not t : ( ( ) ( V11() real ext-real ) Real) <= t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
P : ( ( ) ( ) Subset of ) is connected ;

theorem :: JORDAN1:20
for s1 being ( ( ) ( V11() real ext-real ) Real)
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { |[s : ( ( ) ( V11() real ext-real ) Real) ,t : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s, t is ( ( ) ( V11() real ext-real ) Real) : s1 : ( ( ) ( V11() real ext-real ) Real) < s : ( ( ) ( V11() real ext-real ) Real) } holds
P : ( ( ) ( ) Subset of ) is open ;

theorem :: JORDAN1:21
for s1 being ( ( ) ( V11() real ext-real ) Real)
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { |[s : ( ( ) ( V11() real ext-real ) Real) ,t : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s, t is ( ( ) ( V11() real ext-real ) Real) : s1 : ( ( ) ( V11() real ext-real ) Real) > s : ( ( ) ( V11() real ext-real ) Real) } holds
P : ( ( ) ( ) Subset of ) is open ;

theorem :: JORDAN1:22
for s1 being ( ( ) ( V11() real ext-real ) Real)
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { |[s : ( ( ) ( V11() real ext-real ) Real) ,t : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s, t is ( ( ) ( V11() real ext-real ) Real) : s1 : ( ( ) ( V11() real ext-real ) Real) < t : ( ( ) ( V11() real ext-real ) Real) } holds
P : ( ( ) ( ) Subset of ) is open ;

theorem :: JORDAN1:23
for s1 being ( ( ) ( V11() real ext-real ) Real)
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { |[s : ( ( ) ( V11() real ext-real ) Real) ,t : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s, t is ( ( ) ( V11() real ext-real ) Real) : s1 : ( ( ) ( V11() real ext-real ) Real) > t : ( ( ) ( V11() real ext-real ) Real) } holds
P : ( ( ) ( ) Subset of ) is open ;

theorem :: JORDAN1:24
for s1, t1, s2, t2 being ( ( ) ( V11() real ext-real ) Real)
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { |[s : ( ( ) ( V11() real ext-real ) Real) ,t : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s, t is ( ( ) ( V11() real ext-real ) Real) : ( s1 : ( ( ) ( V11() real ext-real ) Real) < s : ( ( ) ( V11() real ext-real ) Real) & s : ( ( ) ( V11() real ext-real ) Real) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < t : ( ( ) ( V11() real ext-real ) Real) & t : ( ( ) ( V11() real ext-real ) Real) < t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
P : ( ( ) ( ) Subset of ) is open ;

theorem :: JORDAN1:25
for s1, t1, s2, t2 being ( ( ) ( V11() real ext-real ) Real)
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { |[s : ( ( ) ( V11() real ext-real ) Real) ,t : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where s, t is ( ( ) ( V11() real ext-real ) Real) : ( not s1 : ( ( ) ( V11() real ext-real ) Real) <= s : ( ( ) ( V11() real ext-real ) Real) or not s : ( ( ) ( V11() real ext-real ) Real) <= s2 : ( ( ) ( V11() real ext-real ) Real) or not t1 : ( ( ) ( V11() real ext-real ) Real) <= t : ( ( ) ( V11() real ext-real ) Real) or not t : ( ( ) ( V11() real ext-real ) Real) <= t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
P : ( ( ) ( ) Subset of ) is open ;

theorem :: JORDAN1:26
for s1, t1, s2, t2 being ( ( ) ( V11() real ext-real ) Real)
for P, Q being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { |[sa : ( ( ) ( V11() real ext-real ) Real) ,ta : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where sa, ta is ( ( ) ( V11() real ext-real ) Real) : ( s1 : ( ( ) ( V11() real ext-real ) Real) < sa : ( ( ) ( V11() real ext-real ) Real) & sa : ( ( ) ( V11() real ext-real ) Real) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < ta : ( ( ) ( V11() real ext-real ) Real) & ta : ( ( ) ( V11() real ext-real ) Real) < t2 : ( ( ) ( V11() real ext-real ) Real) ) } & Q : ( ( ) ( ) Subset of ) = { |[sb : ( ( ) ( V11() real ext-real ) Real) ,tb : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where sb, tb is ( ( ) ( V11() real ext-real ) Real) : ( not s1 : ( ( ) ( V11() real ext-real ) Real) <= sb : ( ( ) ( V11() real ext-real ) Real) or not sb : ( ( ) ( V11() real ext-real ) Real) <= s2 : ( ( ) ( V11() real ext-real ) Real) or not t1 : ( ( ) ( V11() real ext-real ) Real) <= tb : ( ( ) ( V11() real ext-real ) Real) or not tb : ( ( ) ( V11() real ext-real ) Real) <= t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
P : ( ( ) ( ) Subset of ) misses Q : ( ( ) ( ) Subset of ) ;

theorem :: JORDAN1:27
for s1, s2, t1, t2 being ( ( ) ( V11() real ext-real ) Real) holds { p : ( ( ) ( V11() real ext-real ) Real) where p is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( s1 : ( ( ) ( V11() real ext-real ) Real) < p : ( ( ) ( V11() real ext-real ) Real) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & p : ( ( ) ( V11() real ext-real ) Real) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < p : ( ( ) ( V11() real ext-real ) Real) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & p : ( ( ) ( V11() real ext-real ) Real) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < t2 : ( ( ) ( V11() real ext-real ) Real) ) } = { |[sa : ( ( ) ( V11() real ext-real ) Real) ,ta : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where sa, ta is ( ( ) ( V11() real ext-real ) Real) : ( s1 : ( ( ) ( V11() real ext-real ) Real) < sa : ( ( ) ( V11() real ext-real ) Real) & sa : ( ( ) ( V11() real ext-real ) Real) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < ta : ( ( ) ( V11() real ext-real ) Real) & ta : ( ( ) ( V11() real ext-real ) Real) < t2 : ( ( ) ( V11() real ext-real ) Real) ) } ;

theorem :: JORDAN1:28
for s1, s2, t1, t2 being ( ( ) ( V11() real ext-real ) Real) holds { qc : ( ( ) ( V11() real ext-real ) Real) where qc is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( not s1 : ( ( ) ( V11() real ext-real ) Real) <= qc : ( ( ) ( V11() real ext-real ) Real) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not qc : ( ( ) ( V11() real ext-real ) Real) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) or not t1 : ( ( ) ( V11() real ext-real ) Real) <= qc : ( ( ) ( V11() real ext-real ) Real) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not qc : ( ( ) ( V11() real ext-real ) Real) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) ) } = { |[sb : ( ( ) ( V11() real ext-real ) Real) ,tb : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) where sb, tb is ( ( ) ( V11() real ext-real ) Real) : ( not s1 : ( ( ) ( V11() real ext-real ) Real) <= sb : ( ( ) ( V11() real ext-real ) Real) or not sb : ( ( ) ( V11() real ext-real ) Real) <= s2 : ( ( ) ( V11() real ext-real ) Real) or not t1 : ( ( ) ( V11() real ext-real ) Real) <= tb : ( ( ) ( V11() real ext-real ) Real) or not tb : ( ( ) ( V11() real ext-real ) Real) <= t2 : ( ( ) ( V11() real ext-real ) Real) ) } ;

theorem :: JORDAN1:29
for s1, s2, t1, t2 being ( ( ) ( V11() real ext-real ) Real) holds { p0 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where p0 is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( s1 : ( ( ) ( V11() real ext-real ) Real) < p0 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & p0 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < p0 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & p0 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < t2 : ( ( ) ( V11() real ext-real ) Real) ) } is ( ( ) ( ) Subset of ) ;

theorem :: JORDAN1:30
for s1, s2, t1, t2 being ( ( ) ( V11() real ext-real ) Real) holds { pq : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where pq is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( not s1 : ( ( ) ( V11() real ext-real ) Real) <= pq : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not pq : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) or not t1 : ( ( ) ( V11() real ext-real ) Real) <= pq : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not pq : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) ) } is ( ( ) ( ) Subset of ) ;

theorem :: JORDAN1:31
for s1, t1, s2, t2 being ( ( ) ( V11() real ext-real ) Real)
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { p0 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where p0 is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( s1 : ( ( ) ( V11() real ext-real ) Real) < p0 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & p0 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < p0 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & p0 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
P : ( ( ) ( ) Subset of ) is convex ;

theorem :: JORDAN1:32
for s1, t1, s2, t2 being ( ( ) ( V11() real ext-real ) Real)
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { pq : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where pq is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( not s1 : ( ( ) ( V11() real ext-real ) Real) <= pq : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not pq : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) or not t1 : ( ( ) ( V11() real ext-real ) Real) <= pq : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not pq : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
P : ( ( ) ( ) Subset of ) is connected ;

theorem :: JORDAN1:33
for s1, t1, s2, t2 being ( ( ) ( V11() real ext-real ) Real)
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { p0 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where p0 is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( s1 : ( ( ) ( V11() real ext-real ) Real) < p0 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & p0 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < p0 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & p0 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
P : ( ( ) ( ) Subset of ) is open ;

theorem :: JORDAN1:34
for s1, t1, s2, t2 being ( ( ) ( V11() real ext-real ) Real)
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { pq : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where pq is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( not s1 : ( ( ) ( V11() real ext-real ) Real) <= pq : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not pq : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) or not t1 : ( ( ) ( V11() real ext-real ) Real) <= pq : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not pq : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
P : ( ( ) ( ) Subset of ) is open ;

theorem :: JORDAN1:35
for s1, t1, s2, t2 being ( ( ) ( V11() real ext-real ) Real)
for P, Q being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where p is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( s1 : ( ( ) ( V11() real ext-real ) Real) < p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < t2 : ( ( ) ( V11() real ext-real ) Real) ) } & Q : ( ( ) ( ) Subset of ) = { qc : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where qc is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( not s1 : ( ( ) ( V11() real ext-real ) Real) <= qc : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not qc : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) or not t1 : ( ( ) ( V11() real ext-real ) Real) <= qc : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not qc : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
P : ( ( ) ( ) Subset of ) misses Q : ( ( ) ( ) Subset of ) ;

theorem :: JORDAN1:36
for s1, t1, s2, t2 being ( ( ) ( V11() real ext-real ) Real)
for P, P1, P2 being ( ( ) ( ) Subset of ) st s1 : ( ( ) ( V11() real ext-real ) Real) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < t2 : ( ( ) ( V11() real ext-real ) Real) & P : ( ( ) ( ) Subset of ) = { p : ( ( ) ( ) Subset of ) where p is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( ( p : ( ( ) ( ) Subset of ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( ) Subset of ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( ) Subset of ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( ) Subset of ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( ) Subset of ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( ) Subset of ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t2 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( ) Subset of ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( ) Subset of ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( ) Subset of ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( ) Subset of ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( ) Subset of ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( ) Subset of ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) ) } & P1 : ( ( ) ( ) Subset of ) = { pa : ( ( ) ( ) Subset of ) where pa is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( s1 : ( ( ) ( V11() real ext-real ) Real) < pa : ( ( ) ( ) Subset of ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & pa : ( ( ) ( ) Subset of ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < pa : ( ( ) ( ) Subset of ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & pa : ( ( ) ( ) Subset of ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < t2 : ( ( ) ( V11() real ext-real ) Real) ) } & P2 : ( ( ) ( ) Subset of ) = { pb : ( ( ) ( ) Subset of ) where pb is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( not s1 : ( ( ) ( V11() real ext-real ) Real) <= pb : ( ( ) ( ) Subset of ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not pb : ( ( ) ( ) Subset of ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) or not t1 : ( ( ) ( V11() real ext-real ) Real) <= pb : ( ( ) ( ) Subset of ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not pb : ( ( ) ( ) Subset of ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
( P : ( ( ) ( ) Subset of ) ` : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = P1 : ( ( ) ( ) Subset of ) \/ P2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & P : ( ( ) ( ) Subset of ) ` : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) <> {} : ( ( ) ( empty V163() V164() V165() V166() V167() V168() V169() ) set ) & P1 : ( ( ) ( ) Subset of ) misses P2 : ( ( ) ( ) Subset of ) & ( for P1A, P2B being ( ( ) ( ) Subset of ) st P1A : ( ( ) ( ) Subset of ) = P1 : ( ( ) ( ) Subset of ) & P2B : ( ( ) ( ) Subset of ) = P2 : ( ( ) ( ) Subset of ) holds
( P1A : ( ( ) ( ) Subset of ) is a_component & P2B : ( ( ) ( ) Subset of ) is a_component ) ) ) ;

theorem :: JORDAN1:37
for s1, t1, s2, t2 being ( ( ) ( V11() real ext-real ) Real)
for P, P1, P2 being ( ( ) ( ) Subset of ) st s1 : ( ( ) ( V11() real ext-real ) Real) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < t2 : ( ( ) ( V11() real ext-real ) Real) & P : ( ( ) ( ) Subset of ) = { p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where p is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t2 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) ) } & P1 : ( ( ) ( ) Subset of ) = { pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where pa is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( s1 : ( ( ) ( V11() real ext-real ) Real) < pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < t2 : ( ( ) ( V11() real ext-real ) Real) ) } & P2 : ( ( ) ( ) Subset of ) = { pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where pb is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( not s1 : ( ( ) ( V11() real ext-real ) Real) <= pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) or not t1 : ( ( ) ( V11() real ext-real ) Real) <= pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
( P : ( ( ) ( ) Subset of ) = (Cl P1 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \ P1 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & P : ( ( ) ( ) Subset of ) = (Cl P2 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \ P2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: JORDAN1:38
for s1, s2, t1, t2 being ( ( ) ( V11() real ext-real ) Real)
for P, P1 being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where p is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t2 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) ) } & P1 : ( ( ) ( ) Subset of ) = { pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where pa is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( s1 : ( ( ) ( V11() real ext-real ) Real) < pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
P1 : ( ( ) ( ) Subset of ) c= [#] ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) | (P : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) ) : ( ( ) ( non proper closed ) Element of K6( the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) | (b5 : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: JORDAN1:39
for s1, s2, t1, t2 being ( ( ) ( V11() real ext-real ) Real)
for P, P1 being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where p is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t2 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) ) } & P1 : ( ( ) ( ) Subset of ) = { pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where pa is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( s1 : ( ( ) ( V11() real ext-real ) Real) < pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
P1 : ( ( ) ( ) Subset of ) is ( ( ) ( ) Subset of ) ;

theorem :: JORDAN1:40
for s1, s2, t1, t2 being ( ( ) ( V11() real ext-real ) Real)
for P, P2 being ( ( ) ( ) Subset of ) st s1 : ( ( ) ( V11() real ext-real ) Real) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < t2 : ( ( ) ( V11() real ext-real ) Real) & P : ( ( ) ( ) Subset of ) = { p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where p is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t2 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) ) } & P2 : ( ( ) ( ) Subset of ) = { pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where pb is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( not s1 : ( ( ) ( V11() real ext-real ) Real) <= pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) or not t1 : ( ( ) ( V11() real ext-real ) Real) <= pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
P2 : ( ( ) ( ) Subset of ) c= [#] ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) | (P : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) ) : ( ( ) ( non proper closed ) Element of K6( the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) | (b5 : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: JORDAN1:41
for s1, s2, t1, t2 being ( ( ) ( V11() real ext-real ) Real)
for P, P2 being ( ( ) ( ) Subset of ) st s1 : ( ( ) ( V11() real ext-real ) Real) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < t2 : ( ( ) ( V11() real ext-real ) Real) & P : ( ( ) ( ) Subset of ) = { p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where p is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t2 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) ) } & P2 : ( ( ) ( ) Subset of ) = { pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where pb is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( not s1 : ( ( ) ( V11() real ext-real ) Real) <= pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) or not t1 : ( ( ) ( V11() real ext-real ) Real) <= pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
P2 : ( ( ) ( ) Subset of ) is ( ( ) ( ) Subset of ) ;

begin

definition
let S be ( ( ) ( ) Subset of ) ;
attr S is Jordan means :: JORDAN1:def 2
( S : ( ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital add-continuous Mult-continuous ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital add-continuous Mult-continuous ) RLTopStruct ) ` : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) <> {} : ( ( ) ( empty V163() V164() V165() V166() V167() V168() V169() ) set ) & ex A1, A2 being ( ( ) ( ) Subset of ) st
( S : ( ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital add-continuous Mult-continuous ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital add-continuous Mult-continuous ) RLTopStruct ) ` : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = A1 : ( ( ) ( ) Subset of ) \/ A2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & A1 : ( ( ) ( ) Subset of ) misses A2 : ( ( ) ( ) Subset of ) & (Cl A1 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \ A1 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = (Cl A2 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \ A2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & ( for C1, C2 being ( ( ) ( ) Subset of ) st C1 : ( ( ) ( ) Subset of ) = A1 : ( ( ) ( ) Subset of ) & C2 : ( ( ) ( ) Subset of ) = A2 : ( ( ) ( ) Subset of ) holds
( C1 : ( ( ) ( ) Subset of ) is a_component & C2 : ( ( ) ( ) Subset of ) is a_component ) ) ) );
end;

theorem :: JORDAN1:42
for S being ( ( ) ( ) Subset of ) st S : ( ( ) ( ) Subset of ) is Jordan holds
( S : ( ( ) ( ) Subset of ) ` : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) <> {} : ( ( ) ( empty V163() V164() V165() V166() V167() V168() V169() ) set ) & ex A1, A2 being ( ( ) ( ) Subset of ) ex C1, C2 being ( ( ) ( ) Subset of ) st
( S : ( ( ) ( ) Subset of ) ` : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = A1 : ( ( ) ( ) Subset of ) \/ A2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & A1 : ( ( ) ( ) Subset of ) misses A2 : ( ( ) ( ) Subset of ) & (Cl A1 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \ A1 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = (Cl A2 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \ A2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & C1 : ( ( ) ( ) Subset of ) = A1 : ( ( ) ( ) Subset of ) & C2 : ( ( ) ( ) Subset of ) = A2 : ( ( ) ( ) Subset of ) & C1 : ( ( ) ( ) Subset of ) is a_component & C2 : ( ( ) ( ) Subset of ) is a_component & ( for C3 being ( ( ) ( ) Subset of ) holds
( not C3 : ( ( ) ( ) Subset of ) is a_component or C3 : ( ( ) ( ) Subset of ) = C1 : ( ( ) ( ) Subset of ) or C3 : ( ( ) ( ) Subset of ) = C2 : ( ( ) ( ) Subset of ) ) ) ) ) ;

theorem :: JORDAN1:43
for s1, s2, t1, t2 being ( ( ) ( V11() real ext-real ) Real)
for P being ( ( ) ( ) Subset of ) st s1 : ( ( ) ( V11() real ext-real ) Real) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < t2 : ( ( ) ( V11() real ext-real ) Real) & P : ( ( ) ( ) Subset of ) = { p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where p is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t2 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) ) } holds
P : ( ( ) ( ) Subset of ) is Jordan ;

theorem :: JORDAN1:44
for s1, t1, s2, t2 being ( ( ) ( V11() real ext-real ) Real)
for P, P2 being ( ( ) ( ) Subset of ) st s1 : ( ( ) ( V11() real ext-real ) Real) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < t2 : ( ( ) ( V11() real ext-real ) Real) & P : ( ( ) ( ) Subset of ) = { p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where p is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t2 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) ) } & P2 : ( ( ) ( ) Subset of ) = { pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where pb is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( not s1 : ( ( ) ( V11() real ext-real ) Real) <= pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) or not t1 : ( ( ) ( V11() real ext-real ) Real) <= pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) or not pb : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
Cl P2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = P : ( ( ) ( ) Subset of ) \/ P2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: JORDAN1:45
for s1, t1, s2, t2 being ( ( ) ( V11() real ext-real ) Real)
for P, P1 being ( ( ) ( ) Subset of ) st s1 : ( ( ) ( V11() real ext-real ) Real) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < t2 : ( ( ) ( V11() real ext-real ) Real) & P : ( ( ) ( ) Subset of ) = { p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where p is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t2 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= s1 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = t1 : ( ( ) ( V11() real ext-real ) Real) ) or ( p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) = s2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) <= t2 : ( ( ) ( V11() real ext-real ) Real) & p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) >= t1 : ( ( ) ( V11() real ext-real ) Real) ) ) } & P1 : ( ( ) ( ) Subset of ) = { pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) where pa is ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) : ( s1 : ( ( ) ( V11() real ext-real ) Real) < pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < s2 : ( ( ) ( V11() real ext-real ) Real) & t1 : ( ( ) ( V11() real ext-real ) Real) < pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) & pa : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) < t2 : ( ( ) ( V11() real ext-real ) Real) ) } holds
Cl P1 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = P : ( ( ) ( ) Subset of ) \/ P1 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: JORDAN1:46
for p, q being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) holds (LSeg (p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( non empty connected convex ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \ {p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is convex ;

registration
let p be ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Point of ( ( ) ( non empty ) set ) ) ;
cluster north_halfline p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -> convex ;
cluster east_halfline p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -> convex ;
cluster south_halfline p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -> convex ;
cluster west_halfline p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V112() V155() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V115() V116() V163() V164() V165() V166() V167() V168() ) Element of NAT : ( ( ) ( V163() V164() V165() V166() V167() V168() V169() ) Element of K6(REAL : ( ( ) ( V163() V164() V165() V169() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -> convex ;
end;