A4: Int (left_cell (f,1)) is connected by A1, Th22;
Int (left_cell (f,1)) misses L~ f by A1, GOBOARD8:37;
then A5: Int (left_cell (f,1)) c= (L~ f) ` by SUBSET_1:43;
then (L~ f) ` <> {} by A1, Th18, XBOOLE_1:3;
hence ex b₁ being Subset of (TOP-REAL 2) st
( b₁ is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b₁ ) by A2, A4, A5, Th5; :: thesis: verum