let I be non empty set ; :: thesis: for M being ManySortedSet of I
for X being Subset of
for X1 being SubsetFamily of 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
for X1 being SubsetFamily of 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 ; :: thesis: for X1 being SubsetFamily of 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 ; :: 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 a' = a as Element of by MSUALG_5:def 5;
assume that
A3: a = meet |:X1:| and
A4: b = "/\" X,(EqRelLatt M) ; :: thesis: a = b

A5: now

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

now

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

now

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

end;

now

let q be Element of ; :: 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, A3, Th8;
hence a' [= q by Th7; :: thesis: verum

end;

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