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 A1: P is_inside_component_of L~ g ; :: thesis: P meets RightComp g
A2: BDD (L~ g) = RightComp g by Th47;
A3: P c= BDD (L~ g) by A1, JORDAN2C:26;
P is_a_component_of (L~ g) ` by A1, JORDAN2C:def 3;
hence P meets RightComp g by A2, A3, SPRECT_1:6, XBOOLE_1:67; :: thesis: verum