let f be non constant standard special_circular_sequence; :: thesis: for p being Point of (TOP-REAL 2) holds
( p in LeftComp f iff ( not p in L~ f & not p in RightComp f ) )
let p be Point of (TOP-REAL 2); :: thesis: ( p in LeftComp f iff ( not p in L~ f & not p in RightComp f ) )
A1: (L~ f) ` = (LeftComp f) \/ (RightComp f) by GOBRD12:11;
LeftComp f misses RightComp f by Th24;
then A2: (LeftComp f) /\ (RightComp f) = {} by XBOOLE_0:def 7;
( p in L~ f iff not p in (L~ f) ` ) by XBOOLE_0:def 5;
hence ( p in LeftComp f iff ( not p in L~ f & not p in RightComp f ) ) by A1, A2, XBOOLE_0:def 3, XBOOLE_0:def 4; :: thesis: verum