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|]
now :: thesis: for x being object st x in the carrier of (EqRelLatt M) holds
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;
now :: thesis: for i being object st i in I holds
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;
then x9 c= [|M,M|] by PBOOLE:def 2;
then x9 is ManySortedSubset of [|M,M|] by PBOOLE:def 18;
hence x in Bool [|M,M|] by CLOSURE2:def 1; :: thesis: verum
end;
then the carrier of (EqRelLatt M) c= Bool [|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