let C be Simple_closed_curve; :: thesis: for P being Subset of (TOP-REAL 2)
for U being Subset of ((TOP-REAL 2) | (C ` )) st U = P & U is_a_component_of (TOP-REAL 2) | (C ` ) holds
C = Fr P
let P be Subset of (TOP-REAL 2); :: thesis: for U being Subset of ((TOP-REAL 2) | (C ` )) st U = P & U is_a_component_of (TOP-REAL 2) | (C ` ) holds
C = Fr P
let U be Subset of ((TOP-REAL 2) | (C ` )); :: thesis: ( U = P & U is_a_component_of (TOP-REAL 2) | (C ` ) implies C = Fr P )
not BDD C is empty ;
hence ( U = P & U is_a_component_of (TOP-REAL 2) | (C ` ) implies C = Fr P ) by Lm17; :: thesis: verum