let I be non empty set ; :: thesis: for M being ManySortedSet of holds Top (EqRelLatt M) = [|M,M|]
let M be ManySortedSet of ; :: thesis: Top (EqRelLatt M) = [|M,M|]
set K = [|M,M|];
[|M,M|] is Equivalence_Relation of M by Th3;
then reconsider K = [|M,M|] as Element of (EqRelLatt M) by MSUALG_5:def 5;

now

let a be Element of (EqRelLatt M); :: thesis: ( K "\/" a = K & a "\/" K = K )
reconsider K' = K, a' = a as Equivalence_Relation of M by MSUALG_5:def 5;

A1: now

let i be set ; :: thesis: ( i in I implies (K' "\/" a') . i = K' . i )
assume A2: i in I ; :: thesis: (K' "\/" a') . i = K' . i
then reconsider i' = i as Element of I ;
consider K1 being ManySortedRelation of M such that
A3: ( K1 = K' \/ a' & K' "\/" a' = EqCl K1 ) by MSUALG_5:def 4;
reconsider K2 = K' . i', a2 = a' . i' as Equivalence_Relation of (M . i) by MSUALG_4:def 3;
(K' \/ a') . i = (K' . i) \/ (a' . i) by A2, PBOOLE:def 7
.= [:(M . i),(M . i):] \/ (a' . i) by A2, PBOOLE:def 21
.= (nabla (M . i)) \/ a2 by EQREL_1:def 1
.= nabla (M . i) by EQREL_1:1
.= [:(M . i),(M . i):] by EQREL_1:def 1
.= K' . i by A2, PBOOLE:def 21 ;
hence (K' "\/" a') . i = EqCl K2 by A3, MSUALG_5:def 3
.= K' . i by MSUALG_5:3 ;
:: thesis: verum

end;

thus K "\/" a = the L_join of (EqRelLatt M) . K,a by LATTICES:def 1
.= K' "\/" a' by MSUALG_5:def 5
.= K by A1, PBOOLE:3 ; :: thesis: a "\/" K = K
hence a "\/" K = K ; :: thesis: verum

end;

hence Top (EqRelLatt M) = [|M,M|] by LATTICES:def 17; :: thesis: verum