let X, Y be finite natural-membered set ; :: thesis: ( Y <> {} & ex x being set st
( x in X & {x} <N= Y ) implies (Sgm0 X) . 0 <= (Sgm0 Y) . 0 )
assume A1: ( Y <> {} & ex x being set st
( x in X & {x} <N= Y ) ) ; :: thesis: (Sgm0 X) . 0 <= (Sgm0 Y) . 0
then consider x being set such that
A2: ( x in X & {x} <N= Y ) ;
reconsider x0 = x as Element of NAT by A2, ORDINAL1:def 13;
{x0} c= X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in {x0} or y in X )
assume y in {x0} ; :: thesis: y in X
hence y in X by A2, TARSKI:def 1; :: thesis: verum

end;

then A12: (Sgm0 X) . 0 <= (Sgm0 {x0}) . 0 by AE200;
A4: rng (Sgm0 Y) = Y by AC113;
reconsider X0 = X, Y0 = Y as finite set ;
0 <> card Y by A1;
then 0 < len (Sgm0 Y) by Th44;
then 0 in dom (Sgm0 Y) by NAT_1:45;
then A10: (Sgm0 Y) . 0 in Y by A4, FUNCT_1:def 5;
set nx = x0;
x0 in {x0} by TARSKI:def 1;
then A14: x0 <= (Sgm0 Y) . 0 by A10, A2, AE102;
(Sgm0 {x0}) . 0 = x0 by AE205;
hence (Sgm0 X) . 0 <= (Sgm0 Y) . 0 by A12, A14, XXREAL_0:2; :: thesis: verum