let I be non empty set ; :: thesis: for M being ManySortedSet of I
for X being Subset of ()
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 ()
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 (); :: 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 ;
hence (meet |:X1:|) . i is Relation of (M . i) by ; :: 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 set
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 set ; :: 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 ;
reconsider Q = Q as Subset-Family of [:(M . i),(M . i):] by ;
|:X19:| is V2() ;
then A8: Q <> {} by ;
A9: |:X19:| . i = { (x . i) where x is Element of Bool [|M,M|] : x in X1 } by ;
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 ;
then reconsider Y1 = Y as Relation of (M . i) by ;
z is Equivalence_Relation of M by ;
then Y1 is Equivalence_Relation of (M . i) by ;
hence Y is Equivalence_Relation of (M . i) ; :: thesis: verum
end;
then meet b is Equivalence_Relation of (M . i) by ;
hence R is Equivalence_Relation of (M . i) by ; :: thesis: verum
end;
hence meet |:X1:| is Equivalence_Relation of M by MSUALG_4:def 2; :: thesis: verum