let P be Subset of (TOP-REAL 2); :: thesis: for f being non constant standard special_circular_sequence holds
( not P is_a_component_of (L~ f) ` or P = RightComp f or P = LeftComp f )
let f be non constant standard special_circular_sequence; :: thesis: ( not P is_a_component_of (L~ f) ` or P = RightComp f or P = LeftComp f )
assume P is_a_component_of (L~ f) ` ; :: thesis: ( P = RightComp f or P = LeftComp f )
then ex B1 being Subset of ((TOP-REAL 2) | ((L~ f) `)) st
( B1 = P & B1 is a_component ) by CONNSP_1:def 6;
hence ( P = RightComp f or P = LeftComp f ) by GOBRD14:12; :: thesis: verum