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

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

hence
a c= b
by PBOOLE:def 2; :: thesis: veruma . 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;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