ex c being Element of (CongrLatt A) st
for a being Element of (CongrLatt A) holds
( c "/\" a = c & a "/\" c = c )

proof

reconsider c' = id the Sorts of A as MSCongruence of A by Th19;
reconsider c = c' as Element of (CongrLatt A) by Def6;
take c ; :: thesis: for a being Element of (CongrLatt A) holds
( c "/\" a = c & a "/\" c = c )
let a be Element of (CongrLatt A); :: thesis: ( c "/\" a = c & a "/\" c = c )
reconsider a' = a as MSCongruence of 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 16;
A2: [c,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 (c' /\ a') . i = c' . i )
assume A4: i in the carrier of S ; :: thesis: (c' /\ a') . i = c' . i
then reconsider i' = i as Element of S ;
reconsider a2 = a' . i' as Equivalence_Relation of (the Sorts of A . i) ;
thus (c' /\ a') . i = (c' . i) /\ (a' . i) by A4, PBOOLE:def 8
.= (id (the Sorts of A . i)) /\ a2 by MSUALG_3:def 1
.= id (the Sorts of A . i) by EQREL_1:17
.= c' . i by A4, MSUALG_3:def 1 ; :: thesis: verum

end;

thus c "/\" a = the L_meet of (CongrLatt A) . c,a by LATTICES:def 2
.= the L_meet of (EqRelLatt the Sorts of A) . c,a by A1, A2, FUNCT_1:72
.= c' /\ a' by Def5
.= c by A3, PBOOLE:3 ; :: thesis: a "/\" c = c
hence a "/\" c = c ; :: thesis: verum

end;

then A5: CongrLatt A is lower-bounded by LATTICES:def 13;
ex c being Element of (CongrLatt A) st
for a being Element of (CongrLatt A) holds
( c "\/" a = c & a "\/" c = c )

proof

reconsider c' = [|the Sorts of A,the Sorts of A|] as MSCongruence of A by Th20;
reconsider c = c' as Element of (CongrLatt A) by Def6;
take c ; :: thesis: for a being Element of (CongrLatt A) holds
( c "\/" a = c & a "\/" c = c )
let a be Element of (CongrLatt A); :: thesis: ( c "\/" a = c & a "\/" c = c )
reconsider a' = a as MSCongruence of A by Def6;
A6: 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;
A7: [c,a] in [:the carrier of (CongrLatt A),the carrier of (CongrLatt A):] by ZFMISC_1:106;

A8: now

let i be set ; :: thesis: ( i in the carrier of S implies (c' "\/" a') . i = c' . i )
assume A9: i in the carrier of S ; :: thesis: (c' "\/" a') . i = c' . i
then reconsider i' = i as Element of S ;
consider K1 being ManySortedRelation of the Sorts of A such that
A10: ( K1 = c' \/ a' & c' "\/" a' = EqCl K1 ) by Def4;
reconsider K2 = c' . i', a2 = a' . i' as Equivalence_Relation of (the Sorts of A . i) ;
(c' \/ a') . i = (c' . i) \/ (a' . i) by A9, PBOOLE:def 7
.= (nabla (the Sorts of A . i)) \/ a2 by PBOOLE:def 21
.= nabla (the Sorts of A . i) by EQREL_1:1
.= c' . i by A9, PBOOLE:def 21 ;
hence (c' "\/" a') . i = EqCl K2 by A10, Def3
.= c' . i by Th3 ;
:: thesis: verum

end;

thus c "\/" a = the L_join of (CongrLatt A) . c,a by LATTICES:def 1
.= the L_join of (EqRelLatt the Sorts of A) . c,a by A6, A7, FUNCT_1:72
.= c' "\/" a' by Def5
.= c by A8, PBOOLE:3 ; :: thesis: a "\/" c = c
hence a "\/" c = c ; :: thesis: verum

end;

then CongrLatt A is upper-bounded by LATTICES:def 14;
hence CongrLatt A is bounded by A5; :: thesis: verum