:: JORDAN17 semantic presentation

begin

theorem :: JORDAN17:1
for n being ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) )
for a, p1, p2 being ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) )
for P being ( ( ) ( ) Subset of ) st a : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) in P : ( ( ) ( ) Subset of ) & P : ( ( ) ( ) Subset of ) is_an_arc_of p1 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) holds
ex f being ( ( Function-like V33( the carrier of I[01] : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) : ( ( ) ( ) set ) -valued Function-like V33( the carrier of I[01] : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ex r being ( ( ) ( V11() real ext-real ) Real) st
( f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) : ( ( ) ( ) set ) -valued Function-like V33( the carrier of I[01] : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is being_homeomorphism & f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) : ( ( ) ( ) set ) -valued Function-like V33( the carrier of I[01] : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) . 0 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = p1 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) : ( ( ) ( ) set ) -valued Function-like V33( the carrier of I[01] : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) . 1 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = p2 : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & 0 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) <= r : ( ( ) ( V11() real ext-real ) Real) & r : ( ( ) ( V11() real ext-real ) Real) <= 1 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) & f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of I[01] : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) : ( ( ) ( ) set ) -valued Function-like V33( the carrier of I[01] : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the carrier of ((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) . r : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( ) set ) = a : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ) ;

theorem :: JORDAN17:2
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds LE W-min P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) : ( ( ) ( ) set ) ) , E-max P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) : ( ( ) ( ) set ) ) ,P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) ;

theorem :: JORDAN17:3
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st LE a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) , E-max P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) : ( ( ) ( ) set ) ) ,P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) in Upper_Arc P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) : ( ( V1() ) ( V1() ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: JORDAN17:4
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st LE E-max P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) : ( ( ) ( ) set ) ) ,a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) in Lower_Arc P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) : ( ( V1() ) ( V1() ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: JORDAN17:5
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st LE a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) , W-min P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) : ( ( ) ( ) set ) ) ,P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) in Lower_Arc P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) : ( ( V1() ) ( V1() ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: JORDAN17:6
for a, b, c, d being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) )
for P being ( ( ) ( ) Subset of ) st a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & P : ( ( ) ( ) Subset of ) is_an_arc_of c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & LE a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,P : ( ( ) ( ) Subset of ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) holds
ex e being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st
( a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & LE a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,P : ( ( ) ( ) Subset of ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & LE e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,P : ( ( ) ( ) Subset of ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ) ;

theorem :: JORDAN17:7
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) in P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
ex e being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st
( a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & LE a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) ) ;

theorem :: JORDAN17:8
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a, b being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & LE a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
ex c being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st
( c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & LE a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) & LE c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) ) ;

definition
let P be ( ( ) ( ) Subset of ) ;
let a, b, c, d be ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ;
pred a,b,c,d are_in_this_order_on P means :: JORDAN17:def 1
( ( LE a : ( ( ) ( ) Element of K6(K6(P : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of P : ( ( ) ( ) TopStruct ) ) ,P : ( ( ) ( ) TopStruct ) & LE b : ( ( ) ( ) Element of P : ( ( ) ( ) TopStruct ) ) ,c : ( ( ) ( ) set ) ,P : ( ( ) ( ) TopStruct ) & LE c : ( ( ) ( ) set ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) : ( ( ) ( ) set ) ) ,P : ( ( ) ( ) TopStruct ) ) or ( LE b : ( ( ) ( ) Element of P : ( ( ) ( ) TopStruct ) ) ,c : ( ( ) ( ) set ) ,P : ( ( ) ( ) TopStruct ) & LE c : ( ( ) ( ) set ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) : ( ( ) ( ) set ) ) ,P : ( ( ) ( ) TopStruct ) & LE d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) : ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of K6(K6(P : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,P : ( ( ) ( ) TopStruct ) ) or ( LE c : ( ( ) ( ) set ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) : ( ( ) ( ) set ) ) ,P : ( ( ) ( ) TopStruct ) & LE d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) : ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of K6(K6(P : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,P : ( ( ) ( ) TopStruct ) & LE a : ( ( ) ( ) Element of K6(K6(P : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of P : ( ( ) ( ) TopStruct ) ) ,P : ( ( ) ( ) TopStruct ) ) or ( LE d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) : ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of K6(K6(P : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,P : ( ( ) ( ) TopStruct ) & LE a : ( ( ) ( ) Element of K6(K6(P : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of P : ( ( ) ( ) TopStruct ) ) ,P : ( ( ) ( ) TopStruct ) & LE b : ( ( ) ( ) Element of P : ( ( ) ( ) TopStruct ) ) ,c : ( ( ) ( ) set ) ,P : ( ( ) ( ) TopStruct ) ) );
end;

theorem :: JORDAN17:9
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) in P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) ;

theorem :: JORDAN17:10
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a, b, c, d being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) ;

theorem :: JORDAN17:11
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a, b, c, d being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) ;

theorem :: JORDAN17:12
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a, b, c, d being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) ;

theorem :: JORDAN17:13
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a, b, c, d being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
ex e being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st
( e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) ) ;

theorem :: JORDAN17:14
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a, b, c, d being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
ex e being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st
( e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) ) ;

theorem :: JORDAN17:15
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for b, c, a, d being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
ex e being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st
( e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) ) ;

theorem :: JORDAN17:16
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for b, c, a, d being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
ex e being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st
( e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) ) ;

theorem :: JORDAN17:17
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for c, d, a, b being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
ex e being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st
( e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) ) ;

theorem :: JORDAN17:18
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for c, d, a, b being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
ex e being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st
( e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) ) ;

theorem :: JORDAN17:19
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for d, a, b, c being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
ex e being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st
( e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) ) ;

theorem :: JORDAN17:20
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for d, a, b, c being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
ex e being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st
( e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,e : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) ) ;

theorem :: JORDAN17:21
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a, c, d, b being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) & b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) = b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ;

theorem :: JORDAN17:22
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a, b, c, d being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) & c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) = c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ;

theorem :: JORDAN17:23
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a, b, c, d being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) & d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) = d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ;

theorem :: JORDAN17:24
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a, c, d, b being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) = c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ;

theorem :: JORDAN17:25
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a, b, c, d being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) = d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ;

theorem :: JORDAN17:26
for P being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a, b, c, d being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) <> d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) & a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on P : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) = d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ;

theorem :: JORDAN17:27
for C being ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve)
for a, b, c, d being ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) st a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) in C : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) & b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) in C : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) & c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) in C : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) & d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) in C : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) & not a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on C : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) & not a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on C : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) & not a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on C : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) & not a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on C : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) & not a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on C : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) holds
a : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,d : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,c : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) ,b : ( ( ) ( V43(2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( ) set ) ) are_in_this_order_on C : ( ( being_simple_closed_curve ) ( V1() V75( TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) ) being_simple_closed_curve ) Simple_closed_curve) ;