let g be 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 )
assume A1: P is_outside_component_of L~ g ; :: thesis: P = LeftComp g
UBD (L~ g) is_outside_component_of L~ g by JORDAN2C:68;
then P = UBD (L~ g) by A1, JORDAN2C:119;
hence P = LeftComp g by Th36; :: thesis: verum