theorem :: MSSUBLAT:3

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