let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S holds Bottom (CongrLatt A) = id the Sorts of A

let A be non-empty MSAlgebra over S; :: thesis: Bottom (CongrLatt A) = id the Sorts of A

set K = id the Sorts of A;

id the Sorts of A is MSCongruence of A by Th17;

then reconsider K = id the Sorts of A as Element of (CongrLatt A) by Def6;

A1: the L_meet of (CongrLatt A) = the L_meet of (EqRelLatt the Sorts of A) || the carrier of (CongrLatt A) by NAT_LAT:def 12;

let A be non-empty MSAlgebra over S; :: thesis: Bottom (CongrLatt A) = id the Sorts of A

set K = id the Sorts of A;

id the Sorts of A is MSCongruence of A by Th17;

then reconsider K = id the Sorts of A as Element of (CongrLatt A) by Def6;

A1: the L_meet of (CongrLatt A) = the L_meet 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 )

hence
Bottom (CongrLatt A) = id the Sorts of A
by LATTICES:def 16; :: thesis: verum( 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;

.= the L_meet 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;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

thus K "/\" a =
the L_meet of (CongrLatt A) . (K,a)
by LATTICES:def 2
(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 ;

reconsider a2 = a9 . i9 as Equivalence_Relation of ( the Sorts of A . i) by MSUALG_4:def 2;

thus (K9 (/\) a9) . i = (K9 . i) /\ (a9 . i) by A4, PBOOLE:def 5

.= (id ( the Sorts of A . i)) /\ a2 by MSUALG_3:def 1

.= id ( the Sorts of A . i) by EQREL_1:10

.= K9 . i by A4, MSUALG_3:def 1 ; :: thesis: verum

end;assume A4: i in the carrier of S ; :: thesis: (K9 (/\) a9) . i = K9 . i

then reconsider i9 = i as Element of S ;

reconsider a2 = a9 . i9 as Equivalence_Relation of ( the Sorts of A . i) by MSUALG_4:def 2;

thus (K9 (/\) a9) . i = (K9 . i) /\ (a9 . i) by A4, PBOOLE:def 5

.= (id ( the Sorts of A . i)) /\ a2 by MSUALG_3:def 1

.= id ( the Sorts of A . i) by EQREL_1:10

.= K9 . i by A4, MSUALG_3:def 1 ; :: thesis: verum

.= the L_meet 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