let Y be set ; :: thesis: Top (EqRelLatt Y) = nabla Y
reconsider K = nabla 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_join of (EqRelLatt Y) . (K,a) by LATTICES:def 1
.= (nabla Y) "\/" a9 by MSUALG_5:def 2
.= EqCl ((nabla Y) \/ a9) by MSUALG_5:1
.= EqCl (nabla Y) by EQREL_1:1
.= K by MSUALG_5:2 ; :: thesis: a "\/" K = K
hence a "\/" K = K ; :: thesis: verum

end;

hence Top (EqRelLatt Y) = nabla Y by LATTICES:def 17; :: thesis: verum