let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S holds Top (CongrLatt A) = [| the Sorts of A, the Sorts of A|]
let A be non-empty MSAlgebra over S; :: thesis: Top (CongrLatt A) = [| the Sorts of A, the Sorts of A|]
set K = [| the Sorts of A, the Sorts of A|];
[| the Sorts of A, the Sorts of A|] is MSCongruence of A by Th18;
then reconsider K = [| the Sorts of A, the Sorts of A|] as Element of (CongrLatt A) by Def6;
A1: the L_join of (CongrLatt A) = the L_join of (EqRelLatt the Sorts of A) || the carrier of (CongrLatt A) by NAT_LAT:def 12;

now :: thesis: for a being Element of (CongrLatt A) holds
( K "\/" a = K & a "\/" K = K )

let a be Element of (CongrLatt A); :: thesis: ( K "\/" a = K & a "\/" K = K )
reconsider K9 = K, a9 = a as Equivalence_Relation of the Sorts of A by Def6;
A2: [K,a] in [: the carrier of (CongrLatt A), the carrier of (CongrLatt A):] by ZFMISC_1:87;

A3: now :: thesis: for i being object st i in the carrier of S holds
(K9 "\/" a9) . i = K9 . i

let i be object ; :: thesis: ( i in the carrier of S implies (K9 "\/" a9) . i = K9 . i )
assume A4: i in the carrier of S ; :: thesis: (K9 "\/" a9) . i = K9 . i
then reconsider i9 = i as Element of S ;
A5: ex K1 being ManySortedRelation of the Sorts of A st
( K1 = K9 (\/) a9 & K9 "\/" a9 = EqCl K1 ) by Def4;
reconsider K2 = K9 . i9, a2 = a9 . i9 as Equivalence_Relation of ( the Sorts of A . i) by MSUALG_4:def 2;
(K9 (\/) a9) . i = (K9 . i) \/ (a9 . i) by A4, PBOOLE:def 4
.= (nabla ( the Sorts of A . i)) \/ a2 by PBOOLE:def 16
.= nabla ( the Sorts of A . i) by EQREL_1:1
.= K9 . i by A4, PBOOLE:def 16 ;
hence (K9 "\/" a9) . i = EqCl K2 by A5, Def3
.= K9 . i by Th2 ;
:: thesis: verum

end;

thus K "\/" a = the L_join of (CongrLatt A) . (K,a) by LATTICES:def 1
.= the L_join of (EqRelLatt the Sorts of A) . (K,a) by A1, A2, FUNCT_1:49
.= K9 "\/" a9 by Def5
.= K by A3, PBOOLE:3 ; :: thesis: a "\/" K = K
hence a "\/" K = K ; :: thesis: verum

end;

hence Top (CongrLatt A) = [| the Sorts of A, the Sorts of A|] by LATTICES:def 17; :: thesis: verum