thus RSLattice X is lower-bounded :: according to LATTICES:def 15 :: thesis: RSLattice X is upper-bounded

proof

reconsider E = ERS X as Element of RoughSets X by Lm14;
reconsider e = E as Element of (RSLattice X) by Def23;
take e ; :: according to LATTICES:def 13 :: thesis: for b₁ being Element of the carrier of (RSLattice X) holds
( e "/\" b₁ = e & b₁ "/\" e = e )
let u be Element of (RSLattice X); :: thesis: ( e "/\" u = e & u "/\" e = e )
reconsider K = u as Element of RoughSets X by Def23;
reconsider E9 = E, K9 = K as RoughSet of X by Def20;
e "\/" u = E9 _\/_ K9 by Def23
.= u by Th69 ;
then ( e "/\" u = e & u "/\" e = e ) by LATTICES:def 9;
hence ( e "/\" u = e & u "/\" e = e ) ; :: thesis: verum

end;

thus RSLattice X is upper-bounded :: thesis: verum

proof

reconsider E = TRS X as Element of RoughSets X by Lm15;
reconsider e = E as Element of (RSLattice X) by Def23;
take e ; :: according to LATTICES:def 14 :: thesis: for b₁ being Element of the carrier of (RSLattice X) holds
( e "\/" b₁ = e & b₁ "\/" e = e )
let u be Element of (RSLattice X); :: thesis: ( e "\/" u = e & u "\/" e = e )
reconsider K = u as Element of RoughSets X by Def23;
reconsider E9 = E, K9 = K as RoughSet of X by Def20;
e "/\" u = E9 _/\_ K9 by Def23
.= u by Th70 ;
then ( e "\/" u = e & u "\/" e = e ) by LATTICES:def 8;
hence ( e "\/" u = e & u "\/" e = e ) ; :: thesis: verum

end;