theorem :: AFINSQ_2:26

for X, Y being finite natural-membered set st Y <> {} & ex x being set st
( x in X & {x} <N= Y ) holds
(Sgm0 X) . 0 <= (Sgm0 Y) . 0