let f be rectangular FinSequence of (TOP-REAL 2); :: thesis: LeftComp f misses RightComp f
A1: (L~ f) ` <> {} by Def3;
consider A1, A2 being Subset of (TOP-REAL 2) such that
A2: (L~ f) ` = A1 \/ A2 and
A3: A1 misses A2 and
(Cl A1) \ A1 = (Cl A2) \ A2 and
A4: A1 is_a_component_of (L~ f) ` and
A5: A2 is_a_component_of (L~ f) ` by Def3;
A6: LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
A7: RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def 2;
(L~ f) ` = (LeftComp f) \/ (RightComp f) by GOBRD12:11;
then {(LeftComp f),(RightComp f)} = {A1,A2} by A1, A2, A4, A5, A6, A7, Th9;
then ( ( LeftComp f = A1 & RightComp f = A2 ) or ( LeftComp f = A2 & RightComp f = A1 ) ) by ZFMISC_1:10;
hence LeftComp f misses RightComp f by A3; :: thesis: verum