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₁ being Subset of (TOP-REAL 2) st
( b₁ is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b₁ ) by A3, A6, A7, Th3; :: thesis: verum