A4: Int (left_cell (f,1)) is convex by A1, Th17;
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:23;
then (L~ f) ` <> {} by A1, Th14, 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, Th3; :: thesis: verum