ex c being Element of (EqRelLatt M) st

for a being Element of (EqRelLatt M) holds

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

ex c being Element of (EqRelLatt M) st

for a being Element of (EqRelLatt M) holds

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

hence EqRelLatt M is bounded by A4; :: thesis: verum

for a being Element of (EqRelLatt M) holds

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

proof

then A4:
EqRelLatt M is upper-bounded
by LATTICES:def 14;
reconsider c9 = [|M,M|] as Equivalence_Relation of M by Th2;

reconsider c = c9 as Element of (EqRelLatt M) by MSUALG_5:def 5;

take c ; :: thesis: for a being Element of (EqRelLatt M) holds

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

let a be Element of (EqRelLatt M); :: thesis: ( c "\/" a = c & a "\/" c = c )

reconsider a9 = a as Equivalence_Relation of M by MSUALG_5:def 5;

.= c9 "\/" a9 by MSUALG_5:def 5

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

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

end;reconsider c = c9 as Element of (EqRelLatt M) by MSUALG_5:def 5;

take c ; :: thesis: for a being Element of (EqRelLatt M) holds

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

let a be Element of (EqRelLatt M); :: thesis: ( c "\/" a = c & a "\/" c = c )

reconsider a9 = a as Equivalence_Relation of M by MSUALG_5:def 5;

A1: now :: thesis: for i being object st i in I holds

(c9 "\/" a9) . i = c9 . i

thus c "\/" a =
the L_join of (EqRelLatt M) . (c,a)
by LATTICES:def 1
(c9 "\/" a9) . i = c9 . i

let i be object ; :: thesis: ( i in I implies (c9 "\/" a9) . i = c9 . i )

A2: ex K1 being ManySortedRelation of M st

( K1 = c9 (\/) a9 & c9 "\/" a9 = EqCl K1 ) by MSUALG_5:def 4;

assume A3: i in I ; :: thesis: (c9 "\/" a9) . i = c9 . i

then reconsider i9 = i as Element of I ;

reconsider K2 = c9 . i9, a2 = a9 . i9 as Equivalence_Relation of (M . i) by MSUALG_4:def 2;

(c9 (\/) a9) . i = (c9 . i) \/ (a9 . i) by A3, PBOOLE:def 4

.= [:(M . i),(M . i):] \/ (a9 . i) by A3, PBOOLE:def 16

.= (nabla (M . i)) \/ a2 by EQREL_1:def 1

.= nabla (M . i) by EQREL_1:1

.= [:(M . i),(M . i):] by EQREL_1:def 1

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

hence (c9 "\/" a9) . i = EqCl K2 by A2, MSUALG_5:def 3

.= c9 . i by MSUALG_5:2 ;

:: thesis: verum

end;A2: ex K1 being ManySortedRelation of M st

( K1 = c9 (\/) a9 & c9 "\/" a9 = EqCl K1 ) by MSUALG_5:def 4;

assume A3: i in I ; :: thesis: (c9 "\/" a9) . i = c9 . i

then reconsider i9 = i as Element of I ;

reconsider K2 = c9 . i9, a2 = a9 . i9 as Equivalence_Relation of (M . i) by MSUALG_4:def 2;

(c9 (\/) a9) . i = (c9 . i) \/ (a9 . i) by A3, PBOOLE:def 4

.= [:(M . i),(M . i):] \/ (a9 . i) by A3, PBOOLE:def 16

.= (nabla (M . i)) \/ a2 by EQREL_1:def 1

.= nabla (M . i) by EQREL_1:1

.= [:(M . i),(M . i):] by EQREL_1:def 1

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

hence (c9 "\/" a9) . i = EqCl K2 by A2, MSUALG_5:def 3

.= c9 . i by MSUALG_5:2 ;

:: thesis: verum

.= c9 "\/" a9 by MSUALG_5:def 5

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

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

ex c being Element of (EqRelLatt M) st

for a being Element of (EqRelLatt M) holds

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

proof

then
EqRelLatt M is lower-bounded
by LATTICES:def 13;
reconsider c9 = id M as Equivalence_Relation of M by Th1;

reconsider c = c9 as Element of (EqRelLatt M) by MSUALG_5:def 5;

take c ; :: thesis: for a being Element of (EqRelLatt M) holds

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

let a be Element of (EqRelLatt M); :: thesis: ( c "/\" a = c & a "/\" c = c )

reconsider a9 = a as Equivalence_Relation of M by MSUALG_5:def 5;

.= c9 (/\) a9 by MSUALG_5:def 5

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

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

end;reconsider c = c9 as Element of (EqRelLatt M) by MSUALG_5:def 5;

take c ; :: thesis: for a being Element of (EqRelLatt M) holds

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

let a be Element of (EqRelLatt M); :: thesis: ( c "/\" a = c & a "/\" c = c )

reconsider a9 = a as Equivalence_Relation of M by MSUALG_5:def 5;

A5: now :: thesis: for i being object st i in I holds

(c9 (/\) a9) . i = c9 . i

thus c "/\" a =
the L_meet of (EqRelLatt M) . (c,a)
by LATTICES:def 2
(c9 (/\) a9) . i = c9 . i

let i be object ; :: thesis: ( i in I implies (c9 (/\) a9) . i = c9 . i )

assume A6: i in I ; :: thesis: (c9 (/\) a9) . i = c9 . i

then reconsider i9 = i as Element of I ;

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

thus (c9 (/\) a9) . i = (c9 . i) /\ (a9 . i) by A6, PBOOLE:def 5

.= (id (M . i)) /\ a2 by MSUALG_3:def 1

.= id (M . i) by EQREL_1:10

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

end;assume A6: i in I ; :: thesis: (c9 (/\) a9) . i = c9 . i

then reconsider i9 = i as Element of I ;

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

thus (c9 (/\) a9) . i = (c9 . i) /\ (a9 . i) by A6, PBOOLE:def 5

.= (id (M . i)) /\ a2 by MSUALG_3:def 1

.= id (M . i) by EQREL_1:10

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

.= c9 (/\) a9 by MSUALG_5:def 5

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

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

hence EqRelLatt M is bounded by A4; :: thesis: verum