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