let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S holds Top (CongrLatt A) = [|the Sorts of A,the Sorts of A|]
let A be non-empty MSAlgebra of 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 Th20;
then reconsider K = [|the Sorts of A,the Sorts of A|] as Element of 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 16;

now

let a be Element of ; :: thesis: ( K "\/" a = K & a "\/" K = K )
reconsider K' = K, a' = 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:106;

A3: now

let i be set ; :: thesis: ( i in the carrier of S implies (K' "\/" a') . i = K' . i )
assume A4: i in the carrier of S ; :: thesis: (K' "\/" a') . i = K' . i
then reconsider i' = i as Element of ;
A5: ex K1 being ManySortedRelation of the Sorts of A st
( K1 = K' \/ a' & K' "\/" a' = EqCl K1 ) by Def4;
reconsider K2 = K' . i', a2 = a' . i' as Equivalence_Relation of by MSUALG_4:def 3;
(K' \/ a') . i = (K' . i) \/ (a' . i) by A4, PBOOLE:def 7
.= (nabla (the Sorts of A . i)) \/ a2 by PBOOLE:def 21
.= nabla (the Sorts of A . i) by EQREL_1:1
.= K' . i by A4, PBOOLE:def 21 ;
hence (K' "\/" a') . i = EqCl K2 by A5, Def3
.= K' . i by Th3 ;
:: 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:72
.= K' "\/" a' 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