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 Th22;
reconsider e = E as Element of (RSLattice X) by Def8;
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 Def8;
reconsider E9 = E, K9 = K as RoughSet of X by DefRSX;
e "\/" u = E9 _\/_ K9 by Def8
.= u by Th23 ;
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 Th24;
reconsider e = E as Element of (RSLattice X) by Def8;
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 Def8;
reconsider E9 = E, K9 = K as RoughSet of X by DefRSX;
e "/\" u = E9 _/\_ K9 by Def8
.= u by Th25 ;
then ( e "\/" u = e & u "\/" e = e ) by LATTICES:def 8;
hence ( e "\/" u = e & u "\/" e = e ) ; :: thesis: verum

end;