let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve implies S-min P <> N-max P )
assume A1: P is being_simple_closed_curve ; :: thesis: S-min P <> N-max P
now :: thesis: not S-min P = N-max P
A2: ( |[(lower_bound (proj1 | (S-most P))),(S-bound P)]| = S-min P & |[(upper_bound (proj1 | (N-most P))),(N-bound P)]| = N-max P ) by PSCOMP_1:def 22, PSCOMP_1:def 26;
assume S-min P = N-max P ; :: thesis: contradiction
then S-bound P = N-bound P by A2, SPPOL_2:1;
hence contradiction by A1, Th16; :: thesis: verum
end;
hence S-min P <> N-max P ; :: thesis: verum