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

now

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

end;

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