let C be non empty compact Subset of (TOP-REAL 2); :: thesis: ( C is being_simple_closed_curve implies E-bound C > W-bound C )
assume A1: C is being_simple_closed_curve ; :: thesis: E-bound C > W-bound C

now :: thesis: not E-bound C <= W-bound C

assume A2: E-bound C <= W-bound C ; :: thesis: contradiction
for p being Point of (TOP-REAL 2) st p in C holds
p `1 = W-bound C

proof

let p be Point of (TOP-REAL 2); :: thesis: ( p in C implies p `1 = W-bound C )
assume p in C ; :: thesis: p `1 = W-bound C
then A3: ( W-bound C <= p `1 & p `1 <= E-bound C ) by PSCOMP_1:24;
then W-bound C <= E-bound C by XXREAL_0:2;
then W-bound C = E-bound C by A2, XXREAL_0:1;
hence p `1 = W-bound C by A3, XXREAL_0:1; :: thesis: verum

end;

hence contradiction by A1, Th15; :: thesis: verum

end;

hence E-bound C > W-bound C ; :: thesis: verum