let I be non empty set ; :: thesis: for M being ManySortedSet of I
for X being Subset of (EqRelLatt M)
for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds
meet |:X1:| is Equivalence_Relation of M
let M be ManySortedSet of I; :: thesis: for X being Subset of (EqRelLatt M)
for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds
meet |:X1:| is Equivalence_Relation of M
let X be Subset of (EqRelLatt M); :: thesis: for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds
meet |:X1:| is Equivalence_Relation of M
let X1 be SubsetFamily of [|M,M|]; :: thesis: ( X1 = X & not X is empty implies meet |:X1:| is Equivalence_Relation of M )
set a = meet |:X1:|;

now :: thesis: for i being set st i in I holds
(meet |:X1:|) . i is Relation of (M . i)

let i be set ; :: thesis: ( i in I implies (meet |:X1:|) . i is Relation of (M . i) )
assume A1: i in I ; :: thesis: (meet |:X1:|) . i is Relation of (M . i)
meet |:X1:| c= [|M,M|] by PBOOLE:def 18;
then (meet |:X1:|) . i c= [|M,M|] . i by A1, PBOOLE:def 2;
hence (meet |:X1:|) . i is Relation of (M . i) by A1, PBOOLE:def 16; :: thesis: verum

end;

then reconsider a = meet |:X1:| as ManySortedRelation of M by MSUALG_4:def 1;
assume that
A2: X1 = X and
A3: not X is empty ; :: thesis: meet |:X1:| is Equivalence_Relation of M

now :: thesis: for i being object
for R being Relation of (M . i) st i in I & a . i = R holds
R is Equivalence_Relation of (M . i)

reconsider X19 = X1 as non empty SubsetFamily of [|M,M|] by A2, A3;
let i be object ; :: thesis: for R being Relation of (M . i) st i in I & a . i = R holds
R is Equivalence_Relation of (M . i)
let R be Relation of (M . i); :: thesis: ( i in I & a . i = R implies R is Equivalence_Relation of (M . i) )
assume that
A4: i in I and
A5: a . i = R ; :: thesis: R is Equivalence_Relation of (M . i)
reconsider i9 = i as Element of I by A4;
reconsider b = |:X1:| . i9 as Subset-Family of [:(M . i),(M . i):] by PBOOLE:def 16;
consider Q being Subset-Family of ([|M,M|] . i) such that
A6: Q = |:X1:| . i and
A7: R = Intersect Q by A4, A5, MSSUBFAM:def 1;
reconsider Q = Q as Subset-Family of [:(M . i),(M . i):] by A4, PBOOLE:def 16;
|:X19:| is non-empty ;
then A8: Q <> {} by A4, A6, PBOOLE:def 13;
A9: |:X19:| . i = { (x . i) where x is Element of Bool [|M,M|] : x in X1 } by A4, CLOSURE2:14;

now :: thesis: for Y being set st Y in b holds
Y is Equivalence_Relation of (M . i)

let Y be set ; :: thesis: ( Y in b implies Y is Equivalence_Relation of (M . i) )
assume Y in b ; :: thesis: Y is Equivalence_Relation of (M . i)
then consider z being Element of Bool [|M,M|] such that
A10: Y = z . i and
A11: z in X by A2, A9;
z c= [|M,M|] by PBOOLE:def 18;
then z . i c= [|M,M|] . i by A4, PBOOLE:def 2;
then reconsider Y1 = Y as Relation of (M . i) by A4, A10, PBOOLE:def 16;
z is Equivalence_Relation of M by A11, MSUALG_5:def 5;
then Y1 is Equivalence_Relation of (M . i) by A4, A10, MSUALG_4:def 2;
hence Y is Equivalence_Relation of (M . i) ; :: thesis: verum

end;

then meet b is Equivalence_Relation of (M . i) by A6, A8, EQREL_1:11;
hence R is Equivalence_Relation of (M . i) by A6, A7, A8, SETFAM_1:def 9; :: thesis: verum

end;

hence meet |:X1:| is Equivalence_Relation of M by MSUALG_4:def 2; :: thesis: verum