theorem Th5: :: MSUALG_7:5

for I being non empty set
for M being ManySortedSet of I
for X being Subset of (EqRelLatt M) holds X is SubsetFamily of [|M,M|]