thus LeftComp f is open by Th24; :: according to TOPREAL4:def 3 :: thesis: LeftComp f is connected
LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
then consider A being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that
A1: A = LeftComp f and
A2: A is a_component by CONNSP_1:def 6;
A is connected by A2, CONNSP_1:def 5;
hence LeftComp f is connected by A1, CONNSP_1:23; :: thesis: verum