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