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 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 holds
C = Fr P
let U be Subset of ((TOP-REAL 2) | (C `)); :: thesis: ( U = P & U is a_component implies C = Fr P )
not BDD C is empty ;
hence ( U = P & U is a_component implies C = Fr P ) by Lm15; :: thesis: verum