ex c being Element of () st
for a being Element of () holds
( c "\/" a = c & a "\/" c = c )
proof
reconsider c9 = [| the Sorts of A, the Sorts of A|] as MSCongruence of A by Th18;
A1: the L_join of () = the L_join of (EqRelLatt the Sorts of A) || the carrier of () by NAT_LAT:def 12;
reconsider c = c9 as Element of () by Def6;
take c ; :: thesis: for a being Element of () holds
( c "\/" a = c & a "\/" c = c )

let a be Element of (); :: thesis: ( c "\/" a = c & a "\/" c = c )
A2: [c,a] in [: the carrier of (), the carrier of ():] by ZFMISC_1:87;
reconsider a9 = a as MSCongruence of A by Def6;
A3: now :: thesis: for i being object st i in the carrier of S holds
(c9 "\/" a9) . i = c9 . i
let i be object ; :: thesis: ( i in the carrier of S implies (c9 "\/" a9) . i = c9 . i )
assume A4: i in the carrier of S ; :: thesis: (c9 "\/" a9) . i = c9 . i
then reconsider i9 = i as Element of S ;
A5: ex K1 being ManySortedRelation of the Sorts of A st
( K1 = c9 (\/) a9 & c9 "\/" a9 = EqCl K1 ) by Def4;
reconsider K2 = c9 . i9, a2 = a9 . i9 as Equivalence_Relation of ( the Sorts of A . i) ;
(c9 (\/) a9) . i = (c9 . i) \/ (a9 . i) by
.= (nabla ( the Sorts of A . i)) \/ a2 by PBOOLE:def 16
.= nabla ( the Sorts of A . i) by EQREL_1:1
.= c9 . i by ;
hence (c9 "\/" a9) . i = EqCl K2 by
.= c9 . i by Th2 ;
:: thesis: verum
end;
thus c "\/" a = the L_join of () . (c,a) by LATTICES:def 1
.= the L_join of (EqRelLatt the Sorts of A) . (c,a) by
.= c9 "\/" a9 by Def5
.= c by ; :: thesis: a "\/" c = c
hence a "\/" c = c ; :: thesis: verum
end;
then A6: CongrLatt A is upper-bounded by LATTICES:def 14;
ex c being Element of () st
for a being Element of () holds
( c "/\" a = c & a "/\" c = c )
proof
reconsider c9 = id the Sorts of A as MSCongruence of A by Th17;
A7: the L_meet of () = the L_meet of (EqRelLatt the Sorts of A) || the carrier of () by NAT_LAT:def 12;
reconsider c = c9 as Element of () by Def6;
take c ; :: thesis: for a being Element of () holds
( c "/\" a = c & a "/\" c = c )

let a be Element of (); :: thesis: ( c "/\" a = c & a "/\" c = c )
A8: [c,a] in [: the carrier of (), the carrier of ():] by ZFMISC_1:87;
reconsider a9 = a as MSCongruence of A by Def6;
A9: now :: thesis: for i being object st i in the carrier of S holds
(c9 (/\) a9) . i = c9 . i
let i be object ; :: thesis: ( i in the carrier of S implies (c9 (/\) a9) . i = c9 . i )
assume A10: i in the carrier of S ; :: thesis: (c9 (/\) a9) . i = c9 . i
then reconsider i9 = i as Element of S ;
reconsider a2 = a9 . i9 as Equivalence_Relation of ( the Sorts of A . i) ;
thus (c9 (/\) a9) . i = (c9 . i) /\ (a9 . i) by
.= (id ( the Sorts of A . i)) /\ a2 by MSUALG_3:def 1
.= id ( the Sorts of A . i) by EQREL_1:10
.= c9 . i by ; :: thesis: verum
end;
thus c "/\" a = the L_meet of () . (c,a) by LATTICES:def 2
.= the L_meet of (EqRelLatt the Sorts of A) . (c,a) by
.= c9 (/\) a9 by Def5
.= c by ; :: thesis: a "/\" c = c
hence a "/\" c = c ; :: thesis: verum
end;
then CongrLatt A is lower-bounded by LATTICES:def 13;
hence CongrLatt A is bounded by A6; :: thesis: verum