let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S holds Bottom (CongrLatt A) = id the Sorts of A
let A be non-empty MSAlgebra of S; :: thesis: Bottom (CongrLatt A) = id the Sorts of A
set K = id the Sorts of A;
id the Sorts of A is MSCongruence of A by Th19;
then reconsider K = id the Sorts of A as Element of (CongrLatt A) by Def6;
A1: the L_meet of (CongrLatt A) = the L_meet of (EqRelLatt the Sorts of A) || the carrier of (CongrLatt A) by NAT_LAT:def 16;

now

let a be Element of (CongrLatt A); :: thesis: ( K "/\" a = K & a "/\" K = K )
reconsider K' = K, a' = a as Equivalence_Relation of the Sorts of A by Def6;
A2: [K,a] in [:the carrier of (CongrLatt A),the carrier of (CongrLatt A):] by ZFMISC_1:106;

A3: now

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

end;

thus K "/\" a = the L_meet of (CongrLatt A) . K,a by LATTICES:def 2
.= the L_meet of (EqRelLatt the Sorts of A) . K,a by A1, A2, FUNCT_1:72
.= K' /\ a' by Def5
.= K by A3, PBOOLE:3 ; :: thesis: a "/\" K = K
hence a "/\" K = K ; :: thesis: verum

end;

hence Bottom (CongrLatt A) = id the Sorts of A by LATTICES:def 16; :: thesis: verum