let I be non empty set ; :: thesis: for M being ManySortedSet of I
for X being Subset of ()
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,()) holds
a = b

let M be ManySortedSet of I; :: thesis: for X being Subset of ()
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,()) holds
a = b

let X be Subset of (); :: 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,()) 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,()) 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,()) holds
a = b

let a, b be Equivalence_Relation of M; :: thesis: ( a = meet |:X1:| & b = "/\" (X,()) implies a = b )
reconsider a9 = a as Element of () by MSUALG_5:def 5;
assume that
A3: a = meet |:X1:| and
A4: b = "/\" (X,()) ; :: thesis: a = b
A5: now :: thesis: for c being Element of () 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 (); :: 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 V2() 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 ;
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 () by ;
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 ; :: 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 ; :: thesis: verum
end;
now :: thesis: for q being Element of () st q in X holds
a9 [= q
let q be Element of (); :: 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 ; :: thesis: verum