:: JORDAN16 semantic presentation

begin

theorem :: JORDAN16:1
for C being ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) holds Lower_Arc C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) : ( ( non empty ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) <> Upper_Arc C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) : ( ( non empty ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: JORDAN16:2
for A being ( ( ) ( ) Subset of )
for p1, p2, q1, q2 being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) holds Segment (A : ( ( ) ( ) Subset of ) ,p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) c= A : ( ( ) ( ) Subset of ) ;

theorem :: JORDAN16:3
for A being ( ( ) ( ) Subset of )
for q, p1, p2 being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) st q : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) holds
q : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) in L_Segment (A : ( ( ) ( ) Subset of ) ,p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: JORDAN16:4
for A being ( ( ) ( ) Subset of )
for q, p1, p2 being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) st q : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) holds
q : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) in R_Segment (A : ( ( ) ( ) Subset of ) ,p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: JORDAN16:5
for A being ( ( ) ( ) Subset of )
for q1, q2, p1, p2 being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) st LE q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) Subset of ) ,p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) holds
( q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) in Segment (A : ( ( ) ( ) Subset of ) ,p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) in Segment (A : ( ( ) ( ) Subset of ) ,p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: JORDAN16:6
for C being ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve)
for p, q being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) holds Segment (p : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) c= C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) ;

theorem :: JORDAN16:7
for C being ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve)
for p, q being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) in C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) & q : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) in C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) & not LE p : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) holds
LE q : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) ;

theorem :: JORDAN16:8
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for Y0 being ( ( non empty ) ( non empty TopSpace-like ) SubSpace of Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V29( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like V29( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V29( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like V29( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V29( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous holds
g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like V29( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous ;

theorem :: JORDAN16:9
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for S0 being ( ( non empty ) ( non empty TopSpace-like ) SubSpace of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )
for T0 being ( ( non empty ) ( non empty TopSpace-like ) SubSpace of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V29( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V29( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism holds
for g being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b3 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like V29( the carrier of b3 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b3 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like V29( the carrier of b3 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V29( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) | S0 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b3 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V29( the carrier of b3 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K6(K7( the carrier of b3 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b3 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like V29( the carrier of b3 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is onto holds
g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b3 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like V29( the carrier of b3 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism ;

theorem :: JORDAN16:10
for P1, P2, P3 being ( ( ) ( ) Subset of )
for p1, p2 being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) st P1 : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & P2 : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & P3 : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & P2 : ( ( ) ( ) Subset of ) /\ P3 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = {p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) set ) & P1 : ( ( ) ( ) Subset of ) c= P2 : ( ( ) ( ) Subset of ) \/ P3 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & not P1 : ( ( ) ( ) Subset of ) = P2 : ( ( ) ( ) Subset of ) holds
P1 : ( ( ) ( ) Subset of ) = P3 : ( ( ) ( ) Subset of ) ;

theorem :: JORDAN16:11
for C being ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve)
for A1, A2 being ( ( ) ( ) Subset of )
for p1, p2 being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) st A1 : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & A2 : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & A1 : ( ( ) ( ) Subset of ) c= C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) & A2 : ( ( ) ( ) Subset of ) c= C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) & A1 : ( ( ) ( ) Subset of ) <> A2 : ( ( ) ( ) Subset of ) holds
( A1 : ( ( ) ( ) Subset of ) \/ A2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) & A1 : ( ( ) ( ) Subset of ) /\ A2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = {p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) set ) ) ;

theorem :: JORDAN16:12
for A1, A2 being ( ( ) ( ) Subset of )
for p1, p2, q1, q2 being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) st A1 : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & A1 : ( ( ) ( ) Subset of ) /\ A2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = {q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) set ) holds
A1 : ( ( ) ( ) Subset of ) <> A2 : ( ( ) ( ) Subset of ) ;

theorem :: JORDAN16:13
for C being ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve)
for A1, A2 being ( ( ) ( ) Subset of )
for p1, p2 being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) st A1 : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & A2 : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & A1 : ( ( ) ( ) Subset of ) c= C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) & A2 : ( ( ) ( ) Subset of ) c= C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) & A1 : ( ( ) ( ) Subset of ) /\ A2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = {p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) set ) holds
A1 : ( ( ) ( ) Subset of ) \/ A2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) ;

theorem :: JORDAN16:14
for C being ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve)
for A1, A2 being ( ( ) ( ) Subset of )
for p1, p2 being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) st A1 : ( ( ) ( ) Subset of ) c= C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) & A2 : ( ( ) ( ) Subset of ) c= C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) & A1 : ( ( ) ( ) Subset of ) <> A2 : ( ( ) ( ) Subset of ) & A1 : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & A2 : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) holds
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & A : ( ( ) ( ) Subset of ) c= C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) & not A : ( ( ) ( ) Subset of ) = A1 : ( ( ) ( ) Subset of ) holds
A : ( ( ) ( ) Subset of ) = A2 : ( ( ) ( ) Subset of ) ;

theorem :: JORDAN16:15
for C being ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve)
for A being ( ( non empty ) ( non empty ) Subset of ) st A : ( ( non empty ) ( non empty ) Subset of ) is_an_arc_of W-min C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) , E-max C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) & A : ( ( non empty ) ( non empty ) Subset of ) c= C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) & not A : ( ( non empty ) ( non empty ) Subset of ) = Lower_Arc C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) : ( ( non empty ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) holds
A : ( ( non empty ) ( non empty ) Subset of ) = Upper_Arc C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) : ( ( non empty ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: JORDAN16:16
for A being ( ( ) ( ) Subset of )
for p1, p2, q1, q2 being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & LE q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) Subset of ) ,p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) holds
ex g being ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V111() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) | b1 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( ) set ) ) ex s1, s2 being ( ( ) ( V11() V12() ext-real ) Real) st
( g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V111() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) | b1 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( ) set ) ) is being_homeomorphism & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V111() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) | b1 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( ) set ) ) . 0 : ( ( ) ( empty V10() V11() V12() ext-real non positive non negative Function-like functional V118() V119() V166() V167() V168() V169() V170() V171() V172() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V111() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) | b1 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( ) set ) ) . 1 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V111() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) | b1 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( ) set ) ) . s1 : ( ( ) ( V11() V12() ext-real ) Real) : ( ( ) ( ) set ) = q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V111() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) | b1 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( ) set ) ) . s2 : ( ( ) ( V11() V12() ext-real ) Real) : ( ( ) ( ) set ) = q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & 0 : ( ( ) ( empty V10() V11() V12() ext-real non positive non negative Function-like functional V118() V119() V166() V167() V168() V169() V170() V171() V172() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) <= s1 : ( ( ) ( V11() V12() ext-real ) Real) & s1 : ( ( ) ( V11() V12() ext-real ) Real) <= s2 : ( ( ) ( V11() V12() ext-real ) Real) & s2 : ( ( ) ( V11() V12() ext-real ) Real) <= 1 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: JORDAN16:17
for A being ( ( ) ( ) Subset of )
for p1, p2, q1, q2 being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & LE q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) Subset of ) ,p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) <> q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) holds
ex g being ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V111() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) | b1 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( ) set ) ) ex s1, s2 being ( ( ) ( V11() V12() ext-real ) Real) st
( g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V111() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) | b1 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( ) set ) ) is being_homeomorphism & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V111() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) | b1 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( ) set ) ) . 0 : ( ( ) ( empty V10() V11() V12() ext-real non positive non negative Function-like functional V118() V119() V166() V167() V168() V169() V170() V171() V172() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V111() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) | b1 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( ) set ) ) . 1 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V111() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) | b1 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( ) set ) ) . s1 : ( ( ) ( V11() V12() ext-real ) Real) : ( ( ) ( ) set ) = q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V111() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) | b1 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( ) set ) ) . s2 : ( ( ) ( V11() V12() ext-real ) Real) : ( ( ) ( ) set ) = q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & 0 : ( ( ) ( empty V10() V11() V12() ext-real non positive non negative Function-like functional V118() V119() V166() V167() V168() V169() V170() V171() V172() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) <= s1 : ( ( ) ( V11() V12() ext-real ) Real) & s1 : ( ( ) ( V11() V12() ext-real ) Real) < s2 : ( ( ) ( V11() V12() ext-real ) Real) & s2 : ( ( ) ( V11() V12() ext-real ) Real) <= 1 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: JORDAN16:18
for A being ( ( ) ( ) Subset of )
for q1, q2, p1, p2 being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) st LE q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) Subset of ) ,p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) holds
not Segment (A : ( ( ) ( ) Subset of ) ,p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is empty ;

theorem :: JORDAN16:19
for C being ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve)
for p being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) in C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) holds
( p : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) in Segment (p : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,(W-min C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) ) : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) ,C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & W-min C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) in Segment (p : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,(W-min C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) ) : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) ,C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: JORDAN16:20
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like V29( the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) )
for a, b being ( ( ) ( V11() V12() ext-real ) Real) st a : ( ( ) ( V11() V12() ext-real ) Real) <> 0 : ( ( ) ( empty V10() V11() V12() ext-real non positive non negative Function-like functional V118() V119() V166() V167() V168() V169() V170() V171() V172() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like V29( the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) = AffineMap (a : ( ( ) ( V11() V12() ext-real ) Real) ,b : ( ( ) ( V11() V12() ext-real ) Real) ) : ( ( Function-like quasi_total ) ( non empty Relation-like REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) -defined REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) -valued Function-like V29( REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) quasi_total ) Element of K6(K7(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ,REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like V29( the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V111() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) quasi_total ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) is being_homeomorphism ;

theorem :: JORDAN16:21
for A being ( ( ) ( ) Subset of )
for p1, p2, q1, q2 being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & LE q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) Subset of ) ,p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) <> q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) holds
Segment (A : ( ( ) ( ) Subset of ) ,p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is_an_arc_of q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ;

theorem :: JORDAN16:22
for C being ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve)
for p1, p2 being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) )
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) c= C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) & P : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & W-min C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) Subset of ) & E-max C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) Subset of ) & not Upper_Arc C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) : ( ( non empty ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) c= P : ( ( ) ( ) Subset of ) holds
Lower_Arc C : ( ( being_simple_closed_curve ) ( non empty being_simple_closed_curve compact ) Simple_closed_curve) : ( ( non empty ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) c= P : ( ( ) ( ) Subset of ) ;

theorem :: JORDAN16:23
for P being ( ( ) ( ) Subset of )
for p1, p2, q1, q2 being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) st P : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) Subset of ) & q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( ) ( ) Subset of ) & q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) <> p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) <> p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) <> p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) <> p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) <> q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) holds
ex Q being ( ( non empty ) ( non empty ) Subset of ) st
( Q : ( ( non empty ) ( non empty ) Subset of ) is_an_arc_of q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & Q : ( ( non empty ) ( non empty ) Subset of ) c= P : ( ( ) ( ) Subset of ) & Q : ( ( non empty ) ( non empty ) Subset of ) misses {p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) set ) ) ;

theorem :: JORDAN16:24
for P being ( ( non empty ) ( non empty ) Subset of )
for p1, p2, q1 being ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) st P : ( ( non empty ) ( non empty ) Subset of ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) & q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( non empty ) ( non empty ) Subset of ) & p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) <> q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) holds
Segment (P : ( ( non empty ) ( non empty ) Subset of ) ,p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is_an_arc_of p1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ,q1 : ( ( ) ( V45(2 : ( ( ) ( non empty V10() V11() V12() ext-real positive non negative V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V38() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) V115() V158() ) Point of ( ( ) ( non empty ) set ) ) ;