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

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

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

assume that

A1: LE p,q,C and

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

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

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

assume that

A1: LE p,q,C and

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

per cases
( p = E-max C or p <> E-max C )
;

end;

suppose
p = E-max C
; :: thesis: Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q)

hence
Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q)
by A1, Th9; :: thesis: verum

end;suppose A3:
p <> E-max C
; :: thesis: Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q)

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

A5: q in Lower_Arc C by A1, A2, JORDAN17:4, JORDAN6:58;

A6: p in Lower_Arc C by A2, JORDAN17:4;

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

_{1}[ Point of (TOP-REAL 2)] means ( LE p,$1,C & LE $1,q,C );

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

A12: 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] } ;

A25: { 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(A12);

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

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

end;A5: q in Lower_Arc C by A1, A2, JORDAN17:4, JORDAN6:58;

A6: p in Lower_Arc C by A2, JORDAN17:4;

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

A8: now :: thesis: not p = W-min C

assume A9:
p = W-min C
; :: thesis: contradiction

then LE p, E-max C,C by JORDAN17:2;

hence contradiction by A2, A9, JORDAN6:57, TOPREAL5:19; :: thesis: verum

end;then LE p, E-max C,C by JORDAN17:2;

hence contradiction by A2, A9, JORDAN6:57, TOPREAL5:19; :: thesis: verum

A10: now :: thesis: not q = W-min C

defpred Sassume A11:
q = W-min C
; :: thesis: contradiction

then LE q,p,C by A6, A7, JORDAN7:3;

hence contradiction by A1, A8, A11, JORDAN6:57; :: thesis: verum

end;then LE q,p,C by A6, A7, JORDAN7:3;

hence contradiction by A1, A8, A11, JORDAN6:57; :: thesis: verum

defpred S

A12: 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] )

A21: LE p,p1, Lower_Arc C, E-max C, W-min C and

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

A23: p1 <> W-min C by A4, A10, A22, JORDAN6:55;

A24: p1 in Lower_Arc C by A21, JORDAN5C:def 3;

hence LE p,p1,C by A6, A21, A23, JORDAN6:def 10; :: thesis: LE p1,q,C

thus LE p1,q,C by A5, A10, A22, A24, JORDAN6:def 10; :: thesis: verum

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

assume that assume that

A13: LE p,p1,C and

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

A19: p1 in Lower_Arc C by A13, A17, JORDAN6:def 10;

end;A13: LE p,p1,C and

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

A15: now :: thesis: not p1 = W-min C

assume A16:
p1 = W-min C
; :: thesis: contradiction

then LE p1,p,C by A6, A7, JORDAN7:3;

hence contradiction by A8, A13, A16, JORDAN6:57; :: thesis: verum

end;then LE p1,p,C by A6, A7, JORDAN7:3;

hence contradiction by A8, A13, A16, JORDAN6:57; :: thesis: verum

A17: now :: thesis: not p in Upper_Arc C

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

p in Lower_Arc C by A2, JORDAN17:4;

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

then p in {(W-min C),(E-max C)} by JORDAN6:50;

hence contradiction by A3, A8, TARSKI:def 2; :: thesis: verum

end;p in Lower_Arc C by A2, JORDAN17:4;

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

then p in {(W-min C),(E-max C)} by JORDAN6:50;

hence contradiction by A3, A8, TARSKI:def 2; :: thesis: verum

A19: p1 in Lower_Arc C by A13, A17, JORDAN6:def 10;

per cases
( q = E-max C or p1 = E-max C or p1 <> E-max C )
;

end;

suppose A20:
p1 <> E-max C
; :: thesis: LE p1,q, Lower_Arc C, E-max C, W-min C

end;

now :: thesis: not p1 in Upper_Arc C

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

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

then p1 in {(W-min C),(E-max C)} by JORDAN6:50;

hence contradiction by A15, A20, TARSKI:def 2; :: thesis: verum

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

then p1 in {(W-min C),(E-max C)} by JORDAN6:50;

hence contradiction by A15, A20, TARSKI:def 2; :: thesis: verum

A21: LE p,p1, Lower_Arc C, E-max C, W-min C and

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

A23: p1 <> W-min C by A4, A10, A22, JORDAN6:55;

A24: p1 in Lower_Arc C by A21, JORDAN5C:def 3;

hence LE p,p1,C by A6, A21, A23, JORDAN6:def 10; :: thesis: LE p1,q,C

thus LE p1,q,C by A5, A10, A22, A24, JORDAN6:def 10; :: thesis: verum

set X = { H

set Y = { H

A25: { H

Segment (p,q,C) = { H

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