let g be non constant standard clockwise_oriented special_circular_sequence; :: thesis: for P being Subset of (TOP-REAL 2) st P is_outside_component_of L~ g holds
P = LeftComp g
let P be Subset of (TOP-REAL 2); :: thesis: ( P is_outside_component_of L~ g implies P = LeftComp g )
A1: UBD (L~ g) is_outside_component_of L~ g by JORDAN2C:76;
assume P is_outside_component_of L~ g ; :: thesis: P = LeftComp g
then P = UBD (L~ g) by A1, JORDAN2C:127;
hence P = LeftComp g by Th46; :: thesis: verum