let g be V8() 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

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