let f be V8() standard special_circular_sequence; :: thesis: LeftComp f misses RightComp f

assume (LeftComp f) /\ (RightComp f) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction

then consider x being object such that

A1: x in (LeftComp f) /\ (RightComp f) by XBOOLE_0:def 1;

( LeftComp f is_a_component_of (L~ f) ` & RightComp f is_a_component_of (L~ f) ` ) by GOBOARD9:def 1, GOBOARD9:def 2;

hence contradiction by A2, GOBOARD9:1, SPRECT_4:6; :: thesis: verum

assume (LeftComp f) /\ (RightComp f) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction

then consider x being object such that

A1: x in (LeftComp f) /\ (RightComp f) by XBOOLE_0:def 1;

now :: thesis: ex x being object st

( x in LeftComp f & x in RightComp f )

then A2:
LeftComp f meets RightComp f
by XBOOLE_0:3;( x in LeftComp f & x in RightComp f )

take x = x; :: thesis: ( x in LeftComp f & x in RightComp f )

thus ( x in LeftComp f & x in RightComp f ) by A1, XBOOLE_0:def 4; :: thesis: verum

end;thus ( x in LeftComp f & x in RightComp f ) by A1, XBOOLE_0:def 4; :: thesis: verum

( LeftComp f is_a_component_of (L~ f) ` & RightComp f is_a_component_of (L~ f) ` ) by GOBOARD9:def 1, GOBOARD9:def 2;

hence contradiction by A2, GOBOARD9:1, SPRECT_4:6; :: thesis: verum