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 holds
for a, b being Equivalence_Relation of M st a = meet |:X1:| & b in X holds
a c= b
let M be ManySortedSet of I; :: thesis: for X being Subset of (EqRelLatt M)
for X1 being SubsetFamily of [|M,M|] st X1 = X holds
for a, b being Equivalence_Relation of M st a = meet |:X1:| & b in X holds
a c= b
let X be Subset of (EqRelLatt M); :: thesis: for X1 being SubsetFamily of [|M,M|] st X1 = X holds
for a, b being Equivalence_Relation of M st a = meet |:X1:| & b in X holds
a c= b
let X1 be SubsetFamily of [|M,M|]; :: thesis: ( X1 = X implies for a, b being Equivalence_Relation of M st a = meet |:X1:| & b in X holds
a c= b )
assume A1: X1 = X ; :: thesis: for a, b being Equivalence_Relation of M st a = meet |:X1:| & b in X holds
a c= b
let a, b be Equivalence_Relation of M; :: thesis: ( a = meet |:X1:| & b in X implies a c= b )
assume that
A2: a = meet |:X1:| and
A3: b in X ; :: thesis: a c= b

now :: thesis: for i being object st i in I holds
a . i c= b . i

reconsider b9 = b as Element of Bool [|M,M|] by A1, A3;
let i be object ; :: thesis: ( i in I implies a . i c= b . i )
assume A4: i in I ; :: thesis: a . i c= b . i
then |:X1:| . i = { (x . i) where x is Element of Bool [|M,M|] : x in X1 } by A1, A3, CLOSURE2:14;
then A5: b9 . i in |:X1:| . i by A1, A3;
then A6: for y being object st y in meet (|:X1:| . i) holds
y in b . i by SETFAM_1:def 1;
ex Q being Subset-Family of ([|M,M|] . i) st
( Q = |:X1:| . i & (meet |:X1:|) . i = Intersect Q ) by A4, MSSUBFAM:def 1;
then a . i = meet (|:X1:| . i) by A2, A5, SETFAM_1:def 9;
hence a . i c= b . i by A6; :: thesis: verum

end;

hence a c= b by PBOOLE:def 2; :: thesis: verum