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

proof

reconsider c' = id M as Equivalence_Relation of M by Th2;
reconsider c = c' 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 a' = a as Equivalence_Relation of M by MSUALG_5:def 5;

A1: now

let i be set ; :: thesis: ( i in I implies (c' /\ a') . i = c' . i )
assume A2: i in I ; :: thesis: (c' /\ a') . i = c' . i
then reconsider i' = i as Element of I ;
reconsider a2 = a' . i' as Equivalence_Relation of (M . i) by MSUALG_4:def 3;
thus (c' /\ a') . i = (c' . i) /\ (a' . i) by A2, PBOOLE:def 8
.= (id (M . i)) /\ a2 by MSUALG_3:def 1
.= id (M . i) by EQREL_1:17
.= c' . i by A2, MSUALG_3:def 1 ; :: thesis: verum

end;

thus c "/\" a = the L_meet of (EqRelLatt M) . c,a by LATTICES:def 2
.= c' /\ a' by MSUALG_5:def 5
.= c by A1, PBOOLE:3 ; :: thesis: a "/\" c = c
hence a "/\" c = c ; :: thesis: verum

end;

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

proof

reconsider c' = [|M,M|] as Equivalence_Relation of M by Th3;
reconsider c = c' 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 a' = a as Equivalence_Relation of M by MSUALG_5:def 5;

A4: now

let i be set ; :: thesis: ( i in I implies (c' "\/" a') . i = c' . i )
assume A5: i in I ; :: thesis: (c' "\/" a') . i = c' . i
then reconsider i' = i as Element of I ;
consider K1 being ManySortedRelation of M such that
A6: ( K1 = c' \/ a' & c' "\/" a' = EqCl K1 ) by MSUALG_5:def 4;
reconsider K2 = c' . i', a2 = a' . i' as Equivalence_Relation of (M . i) by MSUALG_4:def 3;
(c' \/ a') . i = (c' . i) \/ (a' . i) by A5, PBOOLE:def 7
.= [:(M . i),(M . i):] \/ (a' . i) by A5, PBOOLE:def 21
.= (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
.= c' . i by A5, PBOOLE:def 21 ;
hence (c' "\/" a') . i = EqCl K2 by A6, MSUALG_5:def 3
.= c' . i by MSUALG_5:3 ;
:: thesis: verum

end;

thus c "\/" a = the L_join of (EqRelLatt M) . c,a by LATTICES:def 1
.= c' "\/" a' by MSUALG_5:def 5
.= c by A4, PBOOLE:3 ; :: thesis: a "\/" c = c
hence a "\/" c = c ; :: thesis: verum

end;

then EqRelLatt M is upper-bounded by LATTICES:def 14;
hence EqRelLatt M is bounded by A3; :: thesis: verum