thus RSLattice X is lower-bounded :: according to LATTICES:def 15 :: thesis:
proof
reconsider E = ERS X as Element of RoughSets X by Lm14;
reconsider e = E as Element of () by Def23;
take e ; :: according to LATTICES:def 13 :: thesis: for b1 being Element of the carrier of () holds
( e "/\" b1 = e & b1 "/\" e = e )

let u be Element of (); :: 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 () by Def23;
take e ; :: according to LATTICES:def 14 :: thesis: for b1 being Element of the carrier of () holds
( e "\/" b1 = e & b1 "\/" e = e )

let u be Element of (); :: 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;