theorem Th35: :: AFINSQ_2:35
for X, Y being finite natural-membered set holds
( X <N< Y iff Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y) )