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;
now :: thesis: ex x being object st
( 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;
then A2: LeftComp f meets RightComp f by XBOOLE_0:3;
( 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