theorem Th21: :: AFINSQ_2:21

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