let f be 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 ) )
LeftComp f misses RightComp f by Th14;
then A1: ( (L~ f) ` = (LeftComp f) \/ (RightComp f) & (LeftComp f) /\ (RightComp f) = {} ) by GOBRD12:10;
( 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, XBOOLE_0:def 3, XBOOLE_0:def 4; :: thesis: verum