theorem Th12: :: HILB10_2:12

for n being Nat
for b being bag of n holds SgmX ((RelIncl n),(support b)) = SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))