theorem Th7: :: MSUALG_8:7

for Y being set
for X being Subset of (EqRelLatt Y) holds union X c= "\/" X