let g be 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 = 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