let I be non empty set ; :: thesis: for M being ManySortedSet of I

for X being Subset of (EqRelLatt M) holds X is SubsetFamily of [|M,M|]

let M be ManySortedSet of I; :: 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|]

then bool the carrier of (EqRelLatt M) c= bool (Bool [|M,M|]) by ZFMISC_1:67;

hence X is SubsetFamily of [|M,M|] ; :: thesis: verum

for X being Subset of (EqRelLatt M) holds X is SubsetFamily of [|M,M|]

let M be ManySortedSet of I; :: 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 :: thesis: for x being object st x in the carrier of (EqRelLatt M) holds

x in Bool [|M,M|]

then
the carrier of (EqRelLatt M) c= Bool [|M,M|]
;x in Bool [|M,M|]

let x be object ; :: 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 x9 = x as Equivalence_Relation of M by MSUALG_5:def 5;

then x9 is ManySortedSubset of [|M,M|] by PBOOLE:def 18;

hence x in Bool [|M,M|] by CLOSURE2:def 1; :: thesis: verum

end;assume x in the carrier of (EqRelLatt M) ; :: thesis: x in Bool [|M,M|]

then reconsider x9 = x as Equivalence_Relation of M by MSUALG_5:def 5;

now :: thesis: for i being object st i in I holds

x9 . i c= [|M,M|] . i

then
x9 c= [|M,M|]
by PBOOLE:def 2;x9 . i c= [|M,M|] . i

let i be object ; :: thesis: ( i in I implies x9 . i c= [|M,M|] . i )

assume i in I ; :: thesis: x9 . i c= [|M,M|] . i

then reconsider i9 = i as Element of I ;

x9 . i9 c= [:(M . i9),(M . i9):] ;

hence x9 . i c= [|M,M|] . i by PBOOLE:def 16; :: thesis: verum

end;assume i in I ; :: thesis: x9 . i c= [|M,M|] . i

then reconsider i9 = i as Element of I ;

x9 . i9 c= [:(M . i9),(M . i9):] ;

hence x9 . i c= [|M,M|] . i by PBOOLE:def 16; :: thesis: verum

then x9 is ManySortedSubset of [|M,M|] by PBOOLE:def 18;

hence x in Bool [|M,M|] by CLOSURE2:def 1; :: thesis: verum

then bool the carrier of (EqRelLatt M) c= bool (Bool [|M,M|]) by ZFMISC_1:67;

hence X is SubsetFamily of [|M,M|] ; :: thesis: verum