theorem Th4: :: HILB10_5:5

for n being Ordinal
for b being bag of n holds degree b = Sum (b * (SgmX ((RelIncl n),(support b))))