let a, b be set ; :: thesis: for f being non constant standard special_circular_sequence holds
( ( ( a in RightComp f & b in RightComp f ) or ( a in LeftComp f & b in LeftComp f ) ) iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & b in C ) )
let f be non constant standard special_circular_sequence; :: thesis: ( ( ( a in RightComp f & b in RightComp f ) or ( a in LeftComp f & b in LeftComp f ) ) iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & b in C ) )
A1: LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
A2: RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def 2;
thus ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not a in C or not b in C ) or ( a in RightComp f & b in RightComp f ) or ( a in LeftComp f & b in LeftComp f ) ) by JORDAN1H:30; :: thesis: ( ( ( a in RightComp f & b in RightComp f ) or ( a in LeftComp f & b in LeftComp f ) ) implies ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & b in C ) )
thus ( ( ( a in RightComp f & b in RightComp f ) or ( a in LeftComp f & b in LeftComp f ) ) implies ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & b in C ) ) by A1, A2; :: thesis: verum