theorem :: MSSUBLAT:2

for a being set holds (*--> a) . 1 = <*a*>