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

( 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