let C be Simple_closed_curve; ( |[(- 1),0]|,|[1,0]| realize-max-dist-in C implies for Jc, Jd being compact with_the_max_arc Subset of (TOP-REAL 2) st Jc is_an_arc_of |[(- 1),0]|,|[1,0]| & Jd is_an_arc_of |[(- 1),0]|,|[1,0]| & C = Jc \/ Jd & Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} & UMP C in Jc & LMP C in Jd & W-bound C = W-bound Jc & E-bound C = E-bound Jc holds
BDD C = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) )
assume A1:
|[(- 1),0]|,|[1,0]| realize-max-dist-in C
; for Jc, Jd being compact with_the_max_arc Subset of (TOP-REAL 2) st Jc is_an_arc_of |[(- 1),0]|,|[1,0]| & Jd is_an_arc_of |[(- 1),0]|,|[1,0]| & C = Jc \/ Jd & Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} & UMP C in Jc & LMP C in Jd & W-bound C = W-bound Jc & E-bound C = E-bound Jc holds
BDD C = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `)))
let Jc, Jd be compact with_the_max_arc Subset of (TOP-REAL 2); ( Jc is_an_arc_of |[(- 1),0]|,|[1,0]| & Jd is_an_arc_of |[(- 1),0]|,|[1,0]| & C = Jc \/ Jd & Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} & UMP C in Jc & LMP C in Jd & W-bound C = W-bound Jc & E-bound C = E-bound Jc implies BDD C = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) )
assume that
A2:
Jc is_an_arc_of |[(- 1),0]|,|[1,0]|
and
A3:
Jd is_an_arc_of |[(- 1),0]|,|[1,0]|
and
A4:
C = Jc \/ Jd
and
A5:
Jc /\ Jd = {|[(- 1),0]|,|[1,0]|}
and
A6:
UMP C in Jc
and
A7:
LMP C in Jd
and
A8:
W-bound C = W-bound Jc
and
A9:
E-bound C = E-bound Jc
; BDD C = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `)))
reconsider Ux = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) as Subset of (TOP-REAL 2) by PRE_TOPC:11;
Ux = BDD C
proof
Ux is_inside_component_of C
by A1, A2, A3, A4, A5, A6, A7, A8, A9, Th95;
hence
Ux c= BDD C
by JORDAN2C:22;
XBOOLE_0:def 10 BDD C c= Ux
set F =
{ B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } ;
let q be
object ;
TARSKI:def 3 ( not q in BDD C or q in Ux )
assume
q in BDD C
;
q in Ux
then consider Z being
set such that A10:
q in Z
and A11:
Z in { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C }
by TARSKI:def 4;
ex
B being
Subset of
(TOP-REAL 2) st
(
Z = B &
B is_inside_component_of C )
by A11;
hence
q in Ux
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, Th95;
verum
end;
hence
BDD C = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `)))
; verum