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