let I be non empty set ; 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; 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); 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|]; ( 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
; 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; ( a = meet |:X1:| & b in X implies a c= b )
assume that
A2:
a = meet |:X1:|
and
A3:
b in X
; a c= b
now for i being object st i in I holds
a . i c= b . ireconsider b9 =
b as
Element of
Bool [|M,M|] by A1, A3;
let i be
object ;
( i in I implies a . i c= b . i )assume A4:
i in I
;
a . i c= b . ithen
|: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;
verum end;
hence
a c= b
by PBOOLE:def 2; verum