let f be non constant standard special_circular_sequence; :: thesis: 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); :: thesis: 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); :: thesis: ( 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 & q in LeftComp f ) and
A2: ( p in g & q in g ) ; :: thesis: g meets L~ f
assume g misses L~ f ; :: thesis: 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:29;
A3: A is connected by CONNSP_1:24;
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
A4: R = RightComp f and
A5: R is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) by CONNSP_1:def 6;
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
A6: L = LeftComp f and
A7: L is_a_component_of (TOP-REAL 2) | ((L~ f) ` ) by CONNSP_1:def 6;
( R /\ A <> {} & L /\ A <> {} ) by A1, A2, A4, A6, XBOOLE_0:def 4;
then ( R meets A & L meets A ) by XBOOLE_0:def 7;
hence contradiction by A3, A4, A5, A6, A7, JORDAN2C:100, SPRECT_4:7; :: thesis: verum