let f be V22() standard special_circular_sequence; for p, q being Point of (TOP-REAL 2)
for g being connected Subset of (TOP-REAL 2) st p in RightComp f & q in LeftComp f & p in g & q in g holds
g meets L~ f
let p, q be Point of (TOP-REAL 2); for g being connected Subset of (TOP-REAL 2) st p in RightComp f & q in LeftComp f & p in g & q in g holds
g meets L~ f
let g be connected Subset of (TOP-REAL 2); ( p in RightComp f & q in LeftComp f & p in g & q in g implies g meets L~ f )
assume that
A1:
p in RightComp f
and
A2:
q in LeftComp f
and
A3:
p in g
and
A4:
q in g
; g meets L~ f
assume
g misses L~ f
; contradiction
then
g c= (L~ f) `
by TDLAT_1:2;
then reconsider A = g as Subset of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8;
RightComp f is_a_component_of (L~ f) `
by GOBOARD9:def 2;
then consider R being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that
A5:
R = RightComp f
and
A6:
R is a_component
by CONNSP_1:def 6;
R /\ A <> {}
by A1, A3, A5, XBOOLE_0:def 4;
then A7:
R meets A
;
LeftComp f is_a_component_of (L~ f) `
by GOBOARD9:def 1;
then consider L being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that
A8:
L = LeftComp f
and
A9:
L is a_component
by CONNSP_1:def 6;
L /\ A <> {}
by A2, A4, A8, XBOOLE_0:def 4;
then A10:
L meets A
;
A is connected
by CONNSP_1:23;
hence
contradiction
by A5, A6, A8, A9, A7, A10, JORDAN2C:92, SPRECT_4:6; verum