let g be V8() standard clockwise_oriented special_circular_sequence; :: thesis: for P being Subset of (TOP-REAL 2) st P is_inside_component_of L~ g holds

P meets RightComp g

let P be Subset of (TOP-REAL 2); :: thesis: ( P is_inside_component_of L~ g implies P meets RightComp g )

assume P is_inside_component_of L~ g ; :: thesis: P meets RightComp g

then A1: ( P c= BDD (L~ g) & P is_a_component_of (L~ g) ` ) by JORDAN2C:22;

BDD (L~ g) = RightComp g by Th37;

hence P meets RightComp g by A1, SPRECT_1:4, XBOOLE_1:67; :: thesis: verum

P meets RightComp g

let P be Subset of (TOP-REAL 2); :: thesis: ( P is_inside_component_of L~ g implies P meets RightComp g )

assume P is_inside_component_of L~ g ; :: thesis: P meets RightComp g

then A1: ( P c= BDD (L~ g) & P is_a_component_of (L~ g) ` ) by JORDAN2C:22;

BDD (L~ g) = RightComp g by Th37;

hence P meets RightComp g by A1, SPRECT_1:4, XBOOLE_1:67; :: thesis: verum