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

hence a = b by A4, A5, LATTICE3:34; :: thesis: verum

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

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 V2() MSSubsetFamily of [|M,M|] ;

assume A6: c is_less_than X ; :: thesis: c [= a9

hence c [= a9 by A3, Th6; :: thesis: verum

end;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 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

then
c9 c= meet |:X1:|
by MSSUBFAM:45;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

end;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

hence
c9 c= Z1
by PBOOLE:def 2; :: thesis: verumc9 . 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;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

hence c [= a9 by A3, Th6; :: thesis: verum

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

a9 [= q

then
a9 is_less_than X
;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;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

hence a = b by A4, A5, LATTICE3:34; :: thesis: verum