thus
RightComp f is open
by Th24; :: according to TOPREAL4:def 3 :: thesis: RightComp f is connected

RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def 2;

then consider A being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that

A3: A = RightComp f and

A4: A is a_component by CONNSP_1:def 6;

A is connected by A4, CONNSP_1:def 5;

hence RightComp f is connected by A3, CONNSP_1:23; :: thesis: verum

RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def 2;

then consider A being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that

A3: A = RightComp f and

A4: A is a_component by CONNSP_1:def 6;

A is connected by A4, CONNSP_1:def 5;

hence RightComp f is connected by A3, CONNSP_1:23; :: thesis: verum