let X, Y be non empty compact Subset of (TOP-REAL 2); :: thesis: ( X c= Y & N-min Y in X implies N-min X = N-min Y )
assume that
A1: X c= Y and
A2: N-min Y in X ; :: thesis: N-min X = N-min Y
A3: N-bound X >= (N-min Y) `2 by A2, PSCOMP_1:24;
A4: (N-min X) `2 = N-bound X by EUCLID:52;
A5: (N-min Y) `2 = N-bound Y by EUCLID:52;
A6: N-bound X <= N-bound Y by A1, PSCOMP_1:66;
then A7: N-bound X = N-bound Y by A5, A3, XXREAL_0:1;
N-min Y in N-most X by A2, A6, A5, A3, SPRECT_2:10, XXREAL_0:1;
then A8: (N-min X) `1 <= (N-min Y) `1 by PSCOMP_1:39;
N-min X in X by SPRECT_1:11;
then N-min X in N-most Y by A1, A6, A4, A5, A3, SPRECT_2:10, XXREAL_0:1;
then (N-min X) `1 >= (N-min Y) `1 by PSCOMP_1:39;
then (N-min X) `1 = (N-min Y) `1 by A8, XXREAL_0:1;
hence N-min X = N-min Y by A4, A5, A7, TOPREAL3:6; :: thesis: verum