let Y be set ; :: thesis: Bottom (EqRelLatt Y) = id Y
reconsider K = id Y as Element of by MSUALG_7:1;

now

let a be Element of ; :: thesis: ( K "/\" a = K & a "/\" K = K )
reconsider a' = a as Equivalence_Relation of by MSUALG_7:1;
thus K "/\" a = the L_meet of (EqRelLatt Y) . K,a by LATTICES:def 2
.= (id Y) /\ a' by MSUALG_5:def 2
.= K by EQREL_1:17 ; :: thesis: a "/\" K = K
hence a "/\" K = K ; :: thesis: verum

end;

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