theorem Th2: :: HILBASIS:2

for b being bag of {} holds decomp b = <*<*{},{}*>*>