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_{1} being Subset of (TOP-REAL 2) st

( b_{1} is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b_{1} )
by A2, A4, A5, Th3; :: thesis: verum

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

( b