:: deftheorem Def4 defines RealSubLatt MSUALG_7:def 4 :
for r1, r2 being Real st r1 <= r2 holds
for b₃ being strict Lattice holds
( b₃ = RealSubLatt (r1,r2) iff ( the carrier of b₃ = [.r1,r2.] & the L_join of b₃ = maxreal || [.r1,r2.] & the L_meet of b₃ = minreal || [.r1,r2.] ) );