theorem Th1: :: MSSUBLAT:1

for a being set holds (*--> a) . 0 = {}