let f be V8() 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

( 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