theorem Th5: :: MSUALG_8:5

for Y being set holds EqRelLatt Y is complete