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

proof

thus
RSLattice X is upper-bounded
:: thesis: verum
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_{1} being Element of the carrier of (RSLattice X) holds

( e "/\" b_{1} = e & b_{1} "/\" 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;reconsider e = E as Element of (RSLattice X) by Def23;

take e ; :: according to LATTICES:def 13 :: thesis: for b

( e "/\" b

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

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_{1} being Element of the carrier of (RSLattice X) holds

( e "\/" b_{1} = e & b_{1} "\/" 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;reconsider e = E as Element of (RSLattice X) by Def23;

take e ; :: according to LATTICES:def 14 :: thesis: for b

( e "\/" b

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