let g be non constant 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, JORDAN2C:def 2;
BDD (L~ g) = RightComp g by Th47;
hence P meets RightComp g by A1, SPRECT_1:4, XBOOLE_1:67; :: thesis: verum