let I be non empty set ; :: thesis: for M being ManySortedSet of
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 ; :: 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 A2:
( a = meet |:X1:| & b in X )
; :: thesis: a c= b
now let i be
set ;
:: thesis: ( i in I implies a . i c= b . i )assume A3:
i in I
;
:: thesis: a . i c= b . ithen A4:
|:X1:| . i = { (x . i) where x is Element of Bool [|M,M|] : x in X1 }
by A1, A2, CLOSURE2:15;
consider Q being
Subset-Family of
([|M,M|] . i) such that A5:
(
Q = |:X1:| . i &
(meet |:X1:|) . i = Intersect Q )
by A3, MSSUBFAM:def 2;
reconsider b' =
b as
Element of
Bool [|M,M|] by A1, A2;
A6:
b' . i in |:X1:| . i
by A1, A2, A4;
then A7:
a . i = meet (|:X1:| . i)
by A2, A5, SETFAM_1:def 10;
for
y being
set st
y in meet (|:X1:| . i) holds
y in b . i
by A6, SETFAM_1:def 1;
hence
a . i c= b . i
by A7, TARSKI:def 3;
:: thesis: verum end;
hence
a c= b
by PBOOLE:def 5; :: thesis: verum