ex c being Element of (EqRelLatt Y) st
for a being Element of (EqRelLatt Y) holds
( c "\/" a = c & a "\/" c = c )
proof
set c9 = nabla Y;
reconsider c = nabla Y as Element of (EqRelLatt Y) by MSUALG_5:21;
take c ; :: thesis: for a being Element of (EqRelLatt Y) holds
( c "\/" a = c & a "\/" c = c )
let a be Element of (EqRelLatt Y); :: thesis: ( c "\/" a = c & a "\/" c = c )
reconsider a9 = a as Equivalence_Relation of Y by MSUALG_5:21;
thus c "\/" a = the L_join of (EqRelLatt Y) . (c,a) by LATTICES:def 1
.= (nabla Y) "\/" a9 by MSUALG_5:def 2
.= EqCl ((nabla Y) \/ a9) by MSUALG_5:1
.= EqCl (nabla Y) by EQREL_1:1
.= c by MSUALG_5:2 ; :: thesis: a "\/" c = c
hence a "\/" c = c ; :: thesis: verum
end;
then A1: EqRelLatt Y is upper-bounded by LATTICES:def 14;
ex c being Element of (EqRelLatt Y) st
for a being Element of (EqRelLatt Y) holds
( c "/\" a = c & a "/\" c = c )
proof
set c9 = id Y;
reconsider c = id Y as Element of (EqRelLatt Y) by MSUALG_5:21;
take c ; :: thesis: for a being Element of (EqRelLatt Y) holds
( c "/\" a = c & a "/\" c = c )
let a be Element of (EqRelLatt Y); :: thesis: ( c "/\" a = c & a "/\" c = c )
reconsider a9 = a as Equivalence_Relation of Y by MSUALG_5:21;
thus c "/\" a = the L_meet of (EqRelLatt Y) . (c,a) by LATTICES:def 2
.= (id Y) /\ a9 by MSUALG_5:def 2
.= c by EQREL_1:10 ; :: thesis: a "/\" c = c
hence a "/\" c = c ; :: thesis: verum
end;
then EqRelLatt Y is lower-bounded by LATTICES:def 13;
hence EqRelLatt Y is bounded by A1; :: thesis: verum