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:50;
then p in (BDD C) \/ (UBD C) by JORDAN2C:31;
then p in UBD C by A2, XBOOLE_0:def 3;
hence contradiction by A4, Th13; :: thesis: verum

end;

end;