let f be constant standard special_circular_sequence; :: thesis: for p being Point of (TOP-REAL 2) holds
( p in L~ f iff ( not p in LeftComp f & not p in RightComp f ) )
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f iff ( not p in LeftComp f & not p in RightComp f ) )
A1: ( p in L~ f iff not p in (L~ f) ` ) by XBOOLE_0:def 5;
(L~ f) ` = (LeftComp f) \/ (RightComp f) by GOBRD12:10;
hence ( p in L~ f iff ( not p in LeftComp f & not p in RightComp f ) ) by A1, XBOOLE_0:def 3; :: thesis: verum