let C be non empty compact Subset of (TOP-REAL 2); :: thesis: ( C is being_simple_closed_curve implies N-bound C > S-bound C )
assume A1: C is being_simple_closed_curve ; :: thesis: N-bound C > S-bound C
now :: thesis: not N-bound C <= S-bound C
assume A2: N-bound C <= S-bound C ; :: thesis: contradiction
for p being Point of (TOP-REAL 2) st p in C holds
p `2 = S-bound C
proof
let p be Point of (TOP-REAL 2); :: thesis: ( p in C implies p `2 = S-bound C )
assume p in C ; :: thesis: p `2 = S-bound C
then A3: ( S-bound C <= p `2 & p `2 <= N-bound C ) by PSCOMP_1:24;
then S-bound C <= N-bound C by XXREAL_0:2;
then S-bound C = N-bound C by A2, XXREAL_0:1;
hence p `2 = S-bound C by A3, XXREAL_0:1; :: thesis: verum
end;
hence contradiction by A1, Th14; :: thesis: verum
end;
hence N-bound C > S-bound C ; :: thesis: verum