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 & 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 I; :: 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 that
A1: X1 = X and
A2: 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 a9 = a as Element of (EqRelLatt M) by MSUALG_5:def 5;
assume that
A3: a = meet |:X1:| and
A4: b = "/\" (X,(EqRelLatt M)) ; :: thesis: a = b

A5: now :: thesis: for c being Element of (EqRelLatt M) st c is_less_than X holds
c [= a9

reconsider X19 = X1 as non empty SubsetFamily of [|M,M|] by A1, A2;
let c be Element of (EqRelLatt M); :: thesis: ( c is_less_than X implies c [= a9 )
reconsider c9 = c as Equivalence_Relation of M by MSUALG_5:def 5;
reconsider S = |:X19:| as non-empty MSSubsetFamily of [|M,M|] ;
assume A6: c is_less_than X ; :: thesis: c [= a9

now :: thesis: for Z1 being ManySortedSet of I st Z1 in S holds
c9 c= Z1

let Z1 be ManySortedSet of I; :: thesis: ( Z1 in S implies c9 c= Z1 )
assume A7: Z1 in S ; :: thesis: c9 c= Z1

now :: thesis: for i being object st i in I holds
c9 . i c= Z1 . i

let i be object ; :: thesis: ( i in I implies c9 . i c= Z1 . i )
assume A8: i in I ; :: thesis: c9 . i c= Z1 . i
then ( Z1 . i in |:X1:| . i & |:X19:| . i = { (x1 . i) where x1 is Element of Bool [|M,M|] : x1 in X1 } ) by A7, CLOSURE2:14, PBOOLE:def 1;
then consider z being Element of Bool [|M,M|] such that
A9: Z1 . i = z . i and
A10: z in X1 ;
reconsider z9 = z as Element of (EqRelLatt M) by A1, A10;
reconsider z1 = z9 as Equivalence_Relation of M by MSUALG_5:def 5;
c [= z9 by A1, A6, A10;
then c9 c= z1 by Th6;
hence c9 . i c= Z1 . i by A8, A9, PBOOLE:def 2; :: thesis: verum

end;

hence c9 c= Z1 by PBOOLE:def 2; :: thesis: verum

end;

then c9 c= meet |:X1:| by MSSUBFAM:45;
hence c [= a9 by A3, Th6; :: thesis: verum

end;

now :: thesis: for q being Element of (EqRelLatt M) st q in X holds
a9 [= q

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

end;

then a9 is_less_than X ;
hence a = b by A4, A5, LATTICE3:34; :: thesis: verum