A6:
Int (right_cell (f,1)) is convex
by A1, Th18;

Int (right_cell (f,1)) misses L~ f by A1, GOBOARD8:38;

then A7: Int (right_cell (f,1)) c= (L~ f) ` by SUBSET_1:23;

then (L~ f) ` <> {} by A1, Th15, XBOOLE_1:3;

hence ex b_{1} being Subset of (TOP-REAL 2) st

( b_{1} is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b_{1} )
by A3, A6, A7, Th3; :: thesis: verum

Int (right_cell (f,1)) misses L~ f by A1, GOBOARD8:38;

then A7: Int (right_cell (f,1)) c= (L~ f) ` by SUBSET_1:23;

then (L~ f) ` <> {} by A1, Th15, XBOOLE_1:3;

hence ex b

( b