let g be V8() 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 = BDD (L~ g)

let P be Subset of (TOP-REAL 2); :: thesis: ( P is_inside_component_of L~ g implies P = BDD (L~ g) )

A1: RightComp g = BDD (L~ g) by Th37;

BDD (L~ g) is_inside_component_of L~ g by JORDAN2C:108;

then A2: BDD (L~ g) is_a_component_of (L~ g) ` ;

assume A3: P is_inside_component_of L~ g ; :: thesis: P = BDD (L~ g)

thus P = BDD (L~ g) by A3, A1, A2, Th39, GOBOARD9:1; :: thesis: verum

P = BDD (L~ g)

let P be Subset of (TOP-REAL 2); :: thesis: ( P is_inside_component_of L~ g implies P = BDD (L~ g) )

A1: RightComp g = BDD (L~ g) by Th37;

BDD (L~ g) is_inside_component_of L~ g by JORDAN2C:108;

then A2: BDD (L~ g) is_a_component_of (L~ g) ` ;

assume A3: P is_inside_component_of L~ g ; :: thesis: P = BDD (L~ g)

thus P = BDD (L~ g) by A3, A1, A2, Th39, GOBOARD9:1; :: thesis: verum