for A being Universal_Algebra
for B being Subset of A holds B |^ 0 = B