let f be non constant 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 set such that
A1: x in (LeftComp f) /\ (RightComp f) by XBOOLE_0:def 1;
A2: LeftComp f meets RightComp f

proof

now

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;

hence LeftComp f meets RightComp f by XBOOLE_0:3; :: thesis: verum

end;

( 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:3, SPRECT_4:7; :: thesis: verum