:: by Adam Grabowski and Yatsuka Nakamura

::

:: Received September 10, 1997

:: Copyright (c) 1997-2012 Association of Mizar Users

begin

theorem Th1: :: JORDAN5C:1

for P, Q being Subset of (TOP-REAL 2)

for p1, p2, q1 being Point of (TOP-REAL 2)

for f being Function of I[01],((TOP-REAL 2) | P)

for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 0 <= t & t < s1 holds

not f . t in Q ) holds

for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= t & t < s2 holds

not g . t in Q

for p1, p2, q1 being Point of (TOP-REAL 2)

for f being Function of I[01],((TOP-REAL 2) | P)

for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 0 <= t & t < s1 holds

not f . t in Q ) holds

for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= t & t < s2 holds

not g . t in Q

proof end;

definition

let P, Q be Subset of (TOP-REAL 2);

let p1, p2 be Point of (TOP-REAL 2);

assume that

A1: ( P meets Q & P /\ Q is closed ) and

A2: P is_an_arc_of p1,p2 ;

ex b_{1} being Point of (TOP-REAL 2) st

( b_{1} in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b_{1} & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= t & t < s2 holds

not g . t in Q ) )

for b_{1}, b_{2} being Point of (TOP-REAL 2) st b_{1} in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b_{1} & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= t & t < s2 holds

not g . t in Q ) & b_{2} in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b_{2} & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= t & t < s2 holds

not g . t in Q ) holds

b_{1} = b_{2}

end;
let p1, p2 be Point of (TOP-REAL 2);

assume that

A1: ( P meets Q & P /\ Q is closed ) and

A2: P is_an_arc_of p1,p2 ;

func First_Point (P,p1,p2,Q) -> Point of (TOP-REAL 2) means :Def1: :: JORDAN5C:def 1

( it in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = it & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= t & t < s2 holds

not g . t in Q ) );

existence ( it in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = it & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= t & t < s2 holds

not g . t in Q ) );

ex b

( b

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b

for t being Real st 0 <= t & t < s2 holds

not g . t in Q ) )

proof end;

uniqueness for b

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b

for t being Real st 0 <= t & t < s2 holds

not g . t in Q ) & b

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b

for t being Real st 0 <= t & t < s2 holds

not g . t in Q ) holds

b

proof end;

:: deftheorem Def1 defines First_Point JORDAN5C:def 1 :

for P, Q being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds

for b_{5} being Point of (TOP-REAL 2) holds

( b_{5} = First_Point (P,p1,p2,Q) iff ( b_{5} in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b_{5} & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= t & t < s2 holds

not g . t in Q ) ) );

for P, Q being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds

for b

( b

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b

for t being Real st 0 <= t & t < s2 holds

not g . t in Q ) ) );

theorem :: JORDAN5C:2

for P, Q being Subset of (TOP-REAL 2)

for p, p1, p2 being Point of (TOP-REAL 2) st p in P & P is_an_arc_of p1,p2 & Q = {p} holds

First_Point (P,p1,p2,Q) = p

for p, p1, p2 being Point of (TOP-REAL 2) st p in P & P is_an_arc_of p1,p2 & Q = {p} holds

First_Point (P,p1,p2,Q) = p

proof end;

theorem Th3: :: JORDAN5C:3

for P, Q being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st p1 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds

First_Point (P,p1,p2,Q) = p1

for p1, p2 being Point of (TOP-REAL 2) st p1 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds

First_Point (P,p1,p2,Q) = p1

proof end;

theorem Th4: :: JORDAN5C:4

for P, Q being Subset of (TOP-REAL 2)

for p1, p2, q1 being Point of (TOP-REAL 2)

for f being Function of I[01],((TOP-REAL 2) | P)

for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds

not f . t in Q ) holds

for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q

for p1, p2, q1 being Point of (TOP-REAL 2)

for f being Function of I[01],((TOP-REAL 2) | P)

for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds

not f . t in Q ) holds

for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q

proof end;

definition

let P, Q be Subset of (TOP-REAL 2);

let p1, p2 be Point of (TOP-REAL 2);

assume that

A1: ( P meets Q & P /\ Q is closed ) and

A2: P is_an_arc_of p1,p2 ;

ex b_{1} being Point of (TOP-REAL 2) st

( b_{1} in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b_{1} & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q ) )

for b_{1}, b_{2} being Point of (TOP-REAL 2) st b_{1} in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b_{1} & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q ) & b_{2} in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b_{2} & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q ) holds

b_{1} = b_{2}

end;
let p1, p2 be Point of (TOP-REAL 2);

assume that

A1: ( P meets Q & P /\ Q is closed ) and

A2: P is_an_arc_of p1,p2 ;

func Last_Point (P,p1,p2,Q) -> Point of (TOP-REAL 2) means :Def2: :: JORDAN5C:def 2

( it in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = it & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q ) );

existence ( it in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = it & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q ) );

ex b

( b

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b

for t being Real st 1 >= t & t > s2 holds

not g . t in Q ) )

proof end;

uniqueness for b

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b

for t being Real st 1 >= t & t > s2 holds

not g . t in Q ) & b

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b

for t being Real st 1 >= t & t > s2 holds

not g . t in Q ) holds

b

proof end;

:: deftheorem Def2 defines Last_Point JORDAN5C:def 2 :

for P, Q being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds

for b_{5} being Point of (TOP-REAL 2) holds

( b_{5} = Last_Point (P,p1,p2,Q) iff ( b_{5} in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b_{5} & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q ) ) );

for P, Q being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds

for b

( b

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b

for t being Real st 1 >= t & t > s2 holds

not g . t in Q ) ) );

theorem :: JORDAN5C:5

for P, Q being Subset of (TOP-REAL 2)

for p, p1, p2 being Point of (TOP-REAL 2) st p in P & P is_an_arc_of p1,p2 & Q = {p} holds

Last_Point (P,p1,p2,Q) = p

for p, p1, p2 being Point of (TOP-REAL 2) st p in P & P is_an_arc_of p1,p2 & Q = {p} holds

Last_Point (P,p1,p2,Q) = p

proof end;

theorem Th6: :: JORDAN5C:6

for P, Q being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st p2 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds

Last_Point (P,p1,p2,Q) = p2

for p1, p2 being Point of (TOP-REAL 2) st p2 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds

Last_Point (P,p1,p2,Q) = p2

proof end;

theorem Th7: :: JORDAN5C:7

for P, Q being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P c= Q & P is closed & P is_an_arc_of p1,p2 holds

( First_Point (P,p1,p2,Q) = p1 & Last_Point (P,p1,p2,Q) = p2 )

for p1, p2 being Point of (TOP-REAL 2) st P c= Q & P is closed & P is_an_arc_of p1,p2 holds

( First_Point (P,p1,p2,Q) = p1 & Last_Point (P,p1,p2,Q) = p2 )

proof end;

begin

:: deftheorem Def3 defines LE JORDAN5C:def 3 :

for P being Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds

( LE q1,q2,P,p1,p2 iff ( q1 in P & q2 in P & ( for g being Function of I[01],((TOP-REAL 2) | P)

for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 holds

s1 <= s2 ) ) );

for P being Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds

( LE q1,q2,P,p1,p2 iff ( q1 in P & q2 in P & ( for g being Function of I[01],((TOP-REAL 2) | P)

for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 holds

s1 <= s2 ) ) );

theorem Th8: :: JORDAN5C:8

for P being Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2)

for g being Function of I[01],((TOP-REAL 2) | P)

for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 holds

LE q1,q2,P,p1,p2

for p1, p2, q1, q2 being Point of (TOP-REAL 2)

for g being Function of I[01],((TOP-REAL 2) | P)

for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 holds

LE q1,q2,P,p1,p2

proof end;

theorem Th9: :: JORDAN5C:9

for P being Subset of (TOP-REAL 2)

for p1, p2, q1 being Point of (TOP-REAL 2) st q1 in P holds

LE q1,q1,P,p1,p2

for p1, p2, q1 being Point of (TOP-REAL 2) st q1 in P holds

LE q1,q1,P,p1,p2

proof end;

theorem Th10: :: JORDAN5C:10

for P being Subset of (TOP-REAL 2)

for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P holds

( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 )

for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P holds

( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 )

proof end;

theorem :: JORDAN5C:11

for P being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

LE p1,p2,P,p1,p2

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

LE p1,p2,P,p1,p2

proof end;

theorem Th12: :: JORDAN5C:12

for P being Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2 holds

q1 = q2

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2 holds

q1 = q2

proof end;

theorem Th13: :: JORDAN5C:13

for P being Subset of (TOP-REAL 2)

for p1, p2, q1, q2, q3 being Point of (TOP-REAL 2) st LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 holds

LE q1,q3,P,p1,p2

for p1, p2, q1, q2, q3 being Point of (TOP-REAL 2) st LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 holds

LE q1,q3,P,p1,p2

proof end;

theorem :: JORDAN5C:14

for P being Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> q2 & not ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) holds

( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 )

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> q2 & not ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) holds

( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 )

proof end;

begin

theorem Th15: :: JORDAN5C:15

for f being FinSequence of (TOP-REAL 2)

for Q being Subset of (TOP-REAL 2)

for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds

LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f)

for Q being Subset of (TOP-REAL 2)

for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds

LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f)

proof end;

theorem Th16: :: JORDAN5C:16

for f being FinSequence of (TOP-REAL 2)

for Q being Subset of (TOP-REAL 2)

for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds

LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f)

for Q being Subset of (TOP-REAL 2)

for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds

LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f)

proof end;

theorem Th17: :: JORDAN5C:17

for q1, q2, p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & LE q1,q2, LSeg (p1,p2),p1,p2 holds

LE q1,q2,p1,p2

LE q1,q2,p1,p2

proof end;

theorem :: JORDAN5C:18

for P, Q being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & P meets Q & P /\ Q is closed holds

( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) )

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & P meets Q & P /\ Q is closed holds

( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) )

proof end;

theorem Th19: :: JORDAN5C:19

for f being FinSequence of (TOP-REAL 2)

for Q being Subset of (TOP-REAL 2)

for i being Element of NAT st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds

First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)

for Q being Subset of (TOP-REAL 2)

for i being Element of NAT st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds

First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)

proof end;

theorem Th20: :: JORDAN5C:20

for f being FinSequence of (TOP-REAL 2)

for Q being Subset of (TOP-REAL 2)

for i being Element of NAT st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds

Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)

for Q being Subset of (TOP-REAL 2)

for i being Element of NAT st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds

Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)

proof end;

theorem :: JORDAN5C:21

for f being FinSequence of (TOP-REAL 2)

for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) holds

First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i

for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) holds

First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i

proof end;

theorem :: JORDAN5C:22

for f being FinSequence of (TOP-REAL 2)

for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) holds

Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1)

for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) holds

Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1)

proof end;

theorem Th23: :: JORDAN5C:23

for f being FinSequence of (TOP-REAL 2)

for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f holds

LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f)

for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f holds

LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f)

proof end;

theorem Th24: :: JORDAN5C:24

for f being FinSequence of (TOP-REAL 2)

for i, j being Element of NAT st f is being_S-Seq & 1 <= i & i <= j & j <= len f holds

LE f /. i,f /. j, L~ f,f /. 1,f /. (len f)

for i, j being Element of NAT st f is being_S-Seq & 1 <= i & i <= j & j <= len f holds

LE f /. i,f /. j, L~ f,f /. 1,f /. (len f)

proof end;

Lm1: for f being FinSequence of (TOP-REAL 2)

for Q being Subset of (TOP-REAL 2)

for q being Point of (TOP-REAL 2)

for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds

LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1)

proof end;

Lm2: for f being FinSequence of (TOP-REAL 2)

for Q being Subset of (TOP-REAL 2)

for q being Point of (TOP-REAL 2)

for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds

LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1)

proof end;

Lm3: for f being FinSequence of (TOP-REAL 2)

for Q being Subset of (TOP-REAL 2)

for q being Point of (TOP-REAL 2)

for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds

LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1)

proof end;

Lm4: for f being FinSequence of (TOP-REAL 2)

for Q being Subset of (TOP-REAL 2)

for q being Point of (TOP-REAL 2)

for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds

LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1)

proof end;

theorem Th25: :: JORDAN5C:25

for f being FinSequence of (TOP-REAL 2)

for q being Point of (TOP-REAL 2)

for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds

LE f /. i,q, L~ f,f /. 1,f /. (len f)

for q being Point of (TOP-REAL 2)

for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds

LE f /. i,q, L~ f,f /. 1,f /. (len f)

proof end;

theorem Th26: :: JORDAN5C:26

for f being FinSequence of (TOP-REAL 2)

for q being Point of (TOP-REAL 2)

for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds

LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f)

for q being Point of (TOP-REAL 2)

for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds

LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f)

proof end;

theorem :: JORDAN5C:27

for f being FinSequence of (TOP-REAL 2)

for Q being Subset of (TOP-REAL 2)

for q being Point of (TOP-REAL 2)

for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds

( i <= j & ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) )

for Q being Subset of (TOP-REAL 2)

for q being Point of (TOP-REAL 2)

for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds

( i <= j & ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) )

proof end;

theorem :: JORDAN5C:28

for f being FinSequence of (TOP-REAL 2)

for Q being Subset of (TOP-REAL 2)

for q being Point of (TOP-REAL 2)

for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds

( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) )

for Q being Subset of (TOP-REAL 2)

for q being Point of (TOP-REAL 2)

for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds

( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) )

proof end;

theorem Th29: :: JORDAN5C:29

for f being FinSequence of (TOP-REAL 2)

for q1, q2 being Point of (TOP-REAL 2)

for i being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) holds

LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1)

for q1, q2 being Point of (TOP-REAL 2)

for i being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) holds

LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1)

proof end;

theorem :: JORDAN5C:30

for f being FinSequence of (TOP-REAL 2)

for q1, q2 being Point of (TOP-REAL 2) st q1 in L~ f & q2 in L~ f & f is being_S-Seq & q1 <> q2 holds

( LE q1,q2, L~ f,f /. 1,f /. (len f) iff for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds

( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) )

for q1, q2 being Point of (TOP-REAL 2) st q1 in L~ f & q2 in L~ f & f is being_S-Seq & q1 <> q2 holds

( LE q1,q2, L~ f,f /. 1,f /. (len f) iff for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds

( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) )

proof end;