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 that
A1: Y <> {} and
A2: ex x being set st
( x in X & {x} <N= Y ) ; :: thesis: (Sgm0 X) . 0 <= (Sgm0 Y) . 0
consider x being set such that
A3: x in X and
A4: {x} <N= Y by A2;
0 <> card Y by A1;
then 0 < len (Sgm0 Y) by Th31;
then A5: 0 in dom (Sgm0 Y) by NAT_1:44;
rng (Sgm0 Y) = Y by Def5;
then A6: (Sgm0 Y) . 0 in Y by A5, FUNCT_1:def 3;
reconsider x0 = x as Element of NAT by A3, ORDINAL1:def 12;
set nx = x0;
x0 in {x0} by TARSKI:def 1;
then A7: x0 <= (Sgm0 Y) . 0 by A4, A6, Def7;
{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 A3, TARSKI:def 1; :: thesis: verum

end;

then A8: (Sgm0 X) . 0 <= (Sgm0 {x0}) . 0 by Th32;
(Sgm0 {x0}) . 0 = x0 by Th33;
hence (Sgm0 X) . 0 <= (Sgm0 Y) . 0 by A8, A7, XXREAL_0:2; :: thesis: verum