let I be non empty set ; :: thesis: for M being ManySortedSet of I holds Bottom (EqRelLatt M) = id M

let M be ManySortedSet of I; :: thesis: Bottom (EqRelLatt M) = id M

set K = id M;

id M is Equivalence_Relation of M by Th1;

then reconsider K = id M as Element of (EqRelLatt M) by MSUALG_5:def 5;

let M be ManySortedSet of I; :: thesis: Bottom (EqRelLatt M) = id M

set K = id M;

id M is Equivalence_Relation of M by Th1;

then reconsider K = id M as Element of (EqRelLatt M) by MSUALG_5:def 5;

now :: thesis: for a being Element of (EqRelLatt M) holds

( K "/\" a = K & a "/\" K = K )

hence
Bottom (EqRelLatt M) = id M
by LATTICES:def 16; :: thesis: verum( K "/\" a = K & a "/\" K = K )

let a be Element of (EqRelLatt M); :: thesis: ( K "/\" a = K & a "/\" K = K )

reconsider K9 = K, a9 = a as Equivalence_Relation of M by MSUALG_5:def 5;

.= K9 (/\) a9 by MSUALG_5:def 5

.= K by A1, PBOOLE:3 ; :: thesis: a "/\" K = K

hence a "/\" K = K ; :: thesis: verum

end;reconsider K9 = K, a9 = a as Equivalence_Relation of M by MSUALG_5:def 5;

A1: now :: thesis: for i being object st i in I holds

(K9 (/\) a9) . i = K9 . i

thus K "/\" a =
the L_meet of (EqRelLatt M) . (K,a)
by LATTICES:def 2
(K9 (/\) a9) . i = K9 . i

let i be object ; :: thesis: ( i in I implies (K9 (/\) a9) . i = K9 . i )

assume A2: i in I ; :: thesis: (K9 (/\) a9) . i = K9 . i

then reconsider i9 = i as Element of I ;

reconsider a2 = a9 . i9 as Equivalence_Relation of (M . i) by MSUALG_4:def 2;

thus (K9 (/\) a9) . i = (K9 . i) /\ (a9 . i) by A2, PBOOLE:def 5

.= (id (M . i)) /\ a2 by MSUALG_3:def 1

.= id (M . i) by EQREL_1:10

.= K9 . i by A2, MSUALG_3:def 1 ; :: thesis: verum

end;assume A2: i in I ; :: thesis: (K9 (/\) a9) . i = K9 . i

then reconsider i9 = i as Element of I ;

reconsider a2 = a9 . i9 as Equivalence_Relation of (M . i) by MSUALG_4:def 2;

thus (K9 (/\) a9) . i = (K9 . i) /\ (a9 . i) by A2, PBOOLE:def 5

.= (id (M . i)) /\ a2 by MSUALG_3:def 1

.= id (M . i) by EQREL_1:10

.= K9 . i by A2, MSUALG_3:def 1 ; :: thesis: verum

.= K9 (/\) a9 by MSUALG_5:def 5

.= K by A1, PBOOLE:3 ; :: thesis: a "/\" K = K

hence a "/\" K = K ; :: thesis: verum