let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st not p in BDD C holds
dist (p,C) <= dist (p,(BDD C))
let p be Point of (TOP-REAL 2); :: thesis: ( not p in BDD C implies dist (p,C) <= dist (p,(BDD C)) )

per cases ( p in C or not p in C ) ;

suppose p in C ; :: thesis: ( not p in BDD C implies dist (p,C) <= dist (p,(BDD C)) )

then dist (p,C) = 0 by JORDAN1K:45;
hence ( not p in BDD C implies dist (p,C) <= dist (p,(BDD C)) ) by JORDAN1K:44; :: thesis: verum

end;

suppose A1: not p in C ; :: thesis: ( not p in BDD C implies dist (p,C) <= dist (p,(BDD C)) )

assume that
A2: not p in BDD C and
A3: dist (p,C) > dist (p,(BDD C)) ; :: thesis: contradiction
A4: ex q being Point of (TOP-REAL 2) st
( q in BDD C & dist (p,q) < dist (p,C) ) by A3, JORDAN1K:48;
p in C ` by A1, SUBSET_1:29;
then p in (BDD C) \/ (UBD C) by JORDAN2C:27;
then p in UBD C by A2, XBOOLE_0:def 3;
hence contradiction by A4, Th13; :: thesis: verum

end;

end;