let I be non empty set ; :: thesis: for M being ManySortedSet of holds Bottom (EqRelLatt M) = id M
let M be ManySortedSet of ; :: thesis: Bottom (EqRelLatt M) = id M
set K = id M;
id M is Equivalence_Relation of M by Th2;
then reconsider K = id M as Element of (EqRelLatt M) by MSUALG_5:def 5;

now

let a be Element of (EqRelLatt M); :: thesis: ( K "/\" a = K & a "/\" K = K )
reconsider K' = K, a' = a as Equivalence_Relation of M by MSUALG_5:def 5;

A1: now

let i be set ; :: thesis: ( i in I implies (K' /\ a') . i = K' . i )
assume A2: i in I ; :: thesis: (K' /\ a') . i = K' . i
then reconsider i' = i as Element of I ;
reconsider a2 = a' . i' as Equivalence_Relation of (M . i) by MSUALG_4:def 3;
thus (K' /\ a') . i = (K' . i) /\ (a' . i) by A2, PBOOLE:def 8
.= (id (M . i)) /\ a2 by MSUALG_3:def 1
.= id (M . i) by EQREL_1:17
.= K' . i by A2, MSUALG_3:def 1 ; :: thesis: verum

end;

thus K "/\" a = the L_meet of (EqRelLatt M) . K,a by LATTICES:def 2
.= K' /\ a' by MSUALG_5:def 5
.= K by A1, PBOOLE:3 ; :: thesis: a "/\" K = K
hence a "/\" K = K ; :: thesis: verum

end;

hence Bottom (EqRelLatt M) = id M by LATTICES:def 16; :: thesis: verum