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 & not X is empty holds
for a, b being Equivalence_Relation of M st a = meet |:X1:| & b = "/\" X,(EqRelLatt M) holds
a = b
let M be ManySortedSet of ; :: thesis: for X being Subset of (EqRelLatt M)
for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds
for a, b being Equivalence_Relation of M st a = meet |:X1:| & b = "/\" X,(EqRelLatt M) holds
a = b
let X be Subset of (EqRelLatt M); :: thesis: for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds
for a, b being Equivalence_Relation of M st a = meet |:X1:| & b = "/\" X,(EqRelLatt M) holds
a = b
let X1 be SubsetFamily of [|M,M|]; :: thesis: ( X1 = X & not X is empty implies for a, b being Equivalence_Relation of M st a = meet |:X1:| & b = "/\" X,(EqRelLatt M) holds
a = b )
assume A1: ( X1 = X & not X is empty ) ; :: thesis: for a, b being Equivalence_Relation of M st a = meet |:X1:| & b = "/\" X,(EqRelLatt M) holds
a = b
let a, b be Equivalence_Relation of M; :: thesis: ( a = meet |:X1:| & b = "/\" X,(EqRelLatt M) implies a = b )
reconsider a' = a as Element of (EqRelLatt M) by MSUALG_5:def 5;
assume A2: ( a = meet |:X1:| & b = "/\" X,(EqRelLatt M) ) ; :: thesis: a = b

now

let q be Element of (EqRelLatt M); :: thesis: ( q in X implies a' [= q )
reconsider q' = q as Equivalence_Relation of M by MSUALG_5:def 5;
assume q in X ; :: thesis: a' [= q
then a c= q' by A1, A2, Th8;
hence a' [= q by Th7; :: thesis: verum

end;

then A3: a' is_less_than X by LATTICE3:def 16;

now

let c be Element of (EqRelLatt M); :: thesis: ( c is_less_than X implies c [= a' )
reconsider c' = c as Equivalence_Relation of M by MSUALG_5:def 5;
assume A4: c is_less_than X ; :: thesis: c [= a'
reconsider X1' = X1 as non empty SubsetFamily of [|M,M|] by A1;
reconsider S = |:X1':| as V2() MSSubsetFamily of [|M,M|] ;

now

let Z1 be ManySortedSet of ; :: thesis: ( Z1 in S implies c' c= Z1 )
assume A5: Z1 in S ; :: thesis: c' c= Z1

now

let i be set ; :: thesis: ( i in I implies c' . i c= Z1 . i )
assume A6: i in I ; :: thesis: c' . i c= Z1 . i
then A7: Z1 . i in |:X1:| . i by A5, PBOOLE:def 4;
|:X1':| . i = { (x1 . i) where x1 is Element of Bool [|M,M|] : x1 in X1 } by A6, CLOSURE2:15;
then consider z being Element of Bool [|M,M|] such that
A8: ( Z1 . i = z . i & z in X1 ) by A7;
reconsider z' = z as Element of (EqRelLatt M) by A1, A8;
reconsider z1 = z' as Equivalence_Relation of M by MSUALG_5:def 5;
c [= z' by A1, A4, A8, LATTICE3:def 16;
then c' c= z1 by Th7;
hence c' . i c= Z1 . i by A6, A8, PBOOLE:def 5; :: thesis: verum

end;

hence c' c= Z1 by PBOOLE:def 5; :: thesis: verum

end;

then c' c= meet |:X1:| by MSSUBFAM:45;
hence c [= a' by A2, Th7; :: thesis: verum

end;

hence a = b by A2, A3, LATTICE3:34; :: thesis: verum