ex c being Element of (CongrLatt A) st

for a being Element of (CongrLatt A) holds

( c "\/" a = c & a "\/" c = c )

ex c being Element of (CongrLatt A) st

for a being Element of (CongrLatt A) holds

( c "/\" a = c & a "/\" c = c )

hence CongrLatt A is bounded by A6; :: thesis: verum

for a being Element of (CongrLatt A) holds

( c "\/" a = c & a "\/" c = c )

proof

then A6:
CongrLatt A is upper-bounded
by LATTICES:def 14;
reconsider c9 = [| the Sorts of A, the Sorts of A|] as MSCongruence of A by Th18;

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;

reconsider c = c9 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 )

A2: [c,a] in [: the carrier of (CongrLatt A), the carrier of (CongrLatt A):] by ZFMISC_1:87;

reconsider a9 = a as MSCongruence of A by Def6;

.= the L_join of (EqRelLatt the Sorts of A) . (c,a) by A1, A2, FUNCT_1:49

.= c9 "\/" a9 by Def5

.= c by A3, PBOOLE:3 ; :: thesis: a "\/" c = c

hence a "\/" c = c ; :: thesis: verum

end;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;

reconsider c = c9 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 )

A2: [c,a] in [: the carrier of (CongrLatt A), the carrier of (CongrLatt A):] 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

thus c "\/" a =
the L_join of (CongrLatt A) . (c,a)
by LATTICES:def 1
(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 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

.= c9 . i by A4, PBOOLE:def 16 ;

hence (c9 "\/" a9) . i = EqCl K2 by A5, Def3

.= c9 . i by Th2 ;

:: thesis: verum

end;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 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

.= c9 . i by A4, PBOOLE:def 16 ;

hence (c9 "\/" a9) . i = EqCl K2 by A5, Def3

.= c9 . i by Th2 ;

:: thesis: verum

.= the L_join of (EqRelLatt the Sorts of A) . (c,a) by A1, A2, FUNCT_1:49

.= c9 "\/" a9 by Def5

.= c by A3, PBOOLE:3 ; :: thesis: a "\/" c = c

hence a "\/" c = c ; :: thesis: verum

ex c being Element of (CongrLatt A) st

for a being Element of (CongrLatt A) holds

( c "/\" a = c & a "/\" c = c )

proof

then
CongrLatt A is lower-bounded
by LATTICES:def 13;
reconsider c9 = id the Sorts of A as MSCongruence of A by Th17;

A7: 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;

reconsider c = c9 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 )

A8: [c,a] in [: the carrier of (CongrLatt A), the carrier of (CongrLatt A):] by ZFMISC_1:87;

reconsider a9 = a as MSCongruence of A by Def6;

.= the L_meet of (EqRelLatt the Sorts of A) . (c,a) by A7, A8, FUNCT_1:49

.= c9 (/\) a9 by Def5

.= c by A9, PBOOLE:3 ; :: thesis: a "/\" c = c

hence a "/\" c = c ; :: thesis: verum

end;A7: 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;

reconsider c = c9 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 )

A8: [c,a] in [: the carrier of (CongrLatt A), the carrier of (CongrLatt A):] 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

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

.= c9 . i by A10, MSUALG_3:def 1 ; :: thesis: verum

end;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 A10, 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

.= c9 . i by A10, MSUALG_3:def 1 ; :: thesis: verum

.= the L_meet of (EqRelLatt the Sorts of A) . (c,a) by A7, A8, FUNCT_1:49

.= c9 (/\) a9 by Def5

.= c by A9, PBOOLE:3 ; :: thesis: a "/\" c = c

hence a "/\" c = c ; :: thesis: verum

hence CongrLatt A is bounded by A6; :: thesis: verum