theorem Th18: :: AOFA_000:18

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