let Y be set ; :: thesis: Bottom (EqRelLatt Y) = id Y
reconsider K = id Y as Element of (EqRelLatt Y) by MSUALG_5:21;
now :: thesis: for a being Element of (EqRelLatt Y) holds
( K "/\" a = K & a "/\" K = K )
let a be Element of (EqRelLatt Y); :: thesis: ( K "/\" a = K & a "/\" K = K )
reconsider a9 = a as Equivalence_Relation of Y by MSUALG_5:21;
thus K "/\" a = the L_meet of (EqRelLatt Y) . (K,a) by LATTICES:def 2
.= (id Y) /\ a9 by MSUALG_5:def 2
.= K by EQREL_1:10 ; :: thesis: a "/\" K = K
hence a "/\" K = K ; :: thesis: verum
end;
hence Bottom (EqRelLatt Y) = id Y by LATTICES:def 16; :: thesis: verum