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

now

let x be set ; :: thesis: ( x in the carrier of (EqRelLatt M) implies x in Bool [|M,M|] )
assume x in the carrier of (EqRelLatt M) ; :: thesis: x in Bool [|M,M|]
then reconsider x' = x as Equivalence_Relation of M by MSUALG_5:def 5;

now

let i be set ; :: thesis: ( i in I implies x' . i c= [|M,M|] . i )
assume i in I ; :: thesis: x' . i c= [|M,M|] . i
then reconsider i' = i as Element of I ;
x' . i' c= [:(M . i'),(M . i'):] ;
hence x' . i c= [|M,M|] . i by PBOOLE:def 21; :: thesis: verum

end;

then x' c= [|M,M|] by PBOOLE:def 5;
then x' is ManySortedSubset of [|M,M|] by PBOOLE:def 23;
hence x in Bool [|M,M|] by CLOSURE2:def 1; :: thesis: verum

end;

then the carrier of (EqRelLatt M) c= Bool [|M,M|] by TARSKI:def 3;
then bool the carrier of (EqRelLatt M) c= bool (Bool [|M,M|]) by ZFMISC_1:79;
hence X is SubsetFamily of [|M,M|] by TARSKI:def 3; :: thesis: verum