let C be Simple_closed_curve; :: thesis: for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds

Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C))

let q be Point of (TOP-REAL 2); :: thesis: ( LE E-max C,q,C implies Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C)) )

set p = W-min C;

assume A1: LE E-max C,q,C ; :: thesis: Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C))

A2: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;

A3: W-min C in Lower_Arc C by JORDAN7:1;

A4: q in Lower_Arc C by A1, JORDAN17:4;

A5: Lower_Arc C c= C by JORDAN6:61;

defpred S_{1}[ Point of (TOP-REAL 2)] means ( LE q,$1,C or ( q in C & $1 = W-min C ) );

defpred S_{2}[ Point of (TOP-REAL 2)] means ( LE q,$1, Lower_Arc C, E-max C, W-min C & LE $1, W-min C, Lower_Arc C, E-max C, W-min C );

A6: for p1 being Point of (TOP-REAL 2) holds

( S_{1}[p1] iff S_{2}[p1] )
_{1}( set ) -> set = $1;

set X = { H_{1}(p1) where p1 is Point of (TOP-REAL 2) : S_{1}[p1] } ;

set Y = { H_{1}(p1) where p1 is Point of (TOP-REAL 2) : S_{2}[p1] } ;

A20: { H_{1}(p1) where p1 is Point of (TOP-REAL 2) : S_{1}[p1] } = { H_{1}(p1) where p1 is Point of (TOP-REAL 2) : S_{2}[p1] }
from FRAENKEL:sch 3(A6);

Segment (q,(W-min C),C) = { H_{1}(p1) where p1 is Point of (TOP-REAL 2) : S_{1}[p1] }
by JORDAN7:def 1;

hence Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C)) by A20, JORDAN6:26; :: thesis: verum

Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C))

let q be Point of (TOP-REAL 2); :: thesis: ( LE E-max C,q,C implies Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C)) )

set p = W-min C;

assume A1: LE E-max C,q,C ; :: thesis: Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C))

A2: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;

A3: W-min C in Lower_Arc C by JORDAN7:1;

A4: q in Lower_Arc C by A1, JORDAN17:4;

A5: Lower_Arc C c= C by JORDAN6:61;

defpred S

defpred S

A6: for p1 being Point of (TOP-REAL 2) holds

( S

proof

deffunc H
let p1 be Point of (TOP-REAL 2); :: thesis: ( S_{1}[p1] iff S_{2}[p1] )

A17: LE q,p1, Lower_Arc C, E-max C, W-min C and

LE p1, W-min C, Lower_Arc C, E-max C, W-min C ; :: thesis: S_{1}[p1]

A18: p1 in Lower_Arc C by A17, JORDAN5C:def 3;

A19: q in Lower_Arc C by A17, JORDAN5C:def 3;

end;hereby :: thesis: ( S_{2}[p1] implies S_{1}[p1] )

assume that assume A7:
( LE q,p1,C or ( q in C & p1 = W-min C ) )
; :: thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )

end;per cases
( ( q = E-max C & LE q,p1,C ) or ( q <> E-max C & LE q,p1,C ) or ( q in C & p1 = W-min C ) )
by A7;

end;

suppose that A8:
q = E-max C
and

A9: LE q,p1,C ; :: thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )

A9: LE q,p1,C ; :: thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )

A10:
p1 in Lower_Arc C
by A8, A9, JORDAN17:4;

hence LE q,p1, Lower_Arc C, E-max C, W-min C by A2, A8, JORDAN5C:10; :: thesis: LE p1, W-min C, Lower_Arc C, E-max C, W-min C

thus LE p1, W-min C, Lower_Arc C, E-max C, W-min C by A2, A10, JORDAN5C:10; :: thesis: verum

end;hence LE q,p1, Lower_Arc C, E-max C, W-min C by A2, A8, JORDAN5C:10; :: thesis: LE p1, W-min C, Lower_Arc C, E-max C, W-min C

thus LE p1, W-min C, Lower_Arc C, E-max C, W-min C by A2, A10, JORDAN5C:10; :: thesis: verum

suppose that A11:
q <> E-max C
and

A12: LE q,p1,C ; :: thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )

A12: LE q,p1,C ; :: thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )

A13:
p1 in Lower_Arc C
by A1, A12, JORDAN17:4, JORDAN6:58;

thus LE p1, W-min C, Lower_Arc C, E-max C, W-min C by A2, A13, JORDAN5C:10; :: thesis: verum

end;A14: now :: thesis: not q = W-min C

assume A15:
q = W-min C
; :: thesis: contradiction

then LE q, E-max C,C by JORDAN7:3, SPRECT_1:14;

hence contradiction by A1, A15, JORDAN6:57, TOPREAL5:19; :: thesis: verum

end;then LE q, E-max C,C by JORDAN7:3, SPRECT_1:14;

hence contradiction by A1, A15, JORDAN6:57, TOPREAL5:19; :: thesis: verum

now :: thesis: not q in Upper_Arc C

hence
LE q,p1, Lower_Arc C, E-max C, W-min C
by A12, JORDAN6:def 10; :: thesis: LE p1, W-min C, Lower_Arc C, E-max C, W-min Cassume
q in Upper_Arc C
; :: thesis: contradiction

then q in (Upper_Arc C) /\ (Lower_Arc C) by A4, XBOOLE_0:def 4;

then q in {(E-max C),(W-min C)} by JORDAN6:def 9;

hence contradiction by A11, A14, TARSKI:def 2; :: thesis: verum

end;then q in (Upper_Arc C) /\ (Lower_Arc C) by A4, XBOOLE_0:def 4;

then q in {(E-max C),(W-min C)} by JORDAN6:def 9;

hence contradiction by A11, A14, TARSKI:def 2; :: thesis: verum

thus LE p1, W-min C, Lower_Arc C, E-max C, W-min C by A2, A13, JORDAN5C:10; :: thesis: verum

suppose that
q in C
and

A16: p1 = W-min C ; :: thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )

A16: p1 = W-min C ; :: thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )

thus
LE q,p1, Lower_Arc C, E-max C, W-min C
by A2, A4, A16, JORDAN5C:10; :: thesis: LE p1, W-min C, Lower_Arc C, E-max C, W-min C

thus LE p1, W-min C, Lower_Arc C, E-max C, W-min C by A3, A16, JORDAN5C:9; :: thesis: verum

end;thus LE p1, W-min C, Lower_Arc C, E-max C, W-min C by A3, A16, JORDAN5C:9; :: thesis: verum

A17: LE q,p1, Lower_Arc C, E-max C, W-min C and

LE p1, W-min C, Lower_Arc C, E-max C, W-min C ; :: thesis: S

A18: p1 in Lower_Arc C by A17, JORDAN5C:def 3;

A19: q in Lower_Arc C by A17, JORDAN5C:def 3;

set X = { H

set Y = { H

A20: { H

Segment (q,(W-min C),C) = { H

hence Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C)) by A20, JORDAN6:26; :: thesis: verum