theorem :: MSUALG_8:3

for Y being set holds Bottom (EqRelLatt Y) = id Y