let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra over S holds MSSubAlLattice U0 is bounded
let U0 be non-empty MSAlgebra over S; :: thesis:
set L = MSSubAlLattice U0;
thus MSSubAlLattice U0 is lower-bounded :: according to LATTICES:def 15 :: thesis:
proof
set C = Constants U0;
reconsider G = GenMSAlg () as Element of MSSub U0 by Def19;
reconsider G1 = G as Element of () ;
take G1 ; :: according to LATTICES:def 13 :: thesis: for b1 being Element of the carrier of () holds
( G1 "/\" b1 = G1 & b1 "/\" G1 = G1 )

let a be Element of (); :: thesis: ( G1 "/\" a = G1 & a "/\" G1 = G1 )
reconsider a1 = a as Element of MSSub U0 ;
reconsider a2 = a1 as strict MSSubAlgebra of U0 by Def19;
thus G1 "/\" a = (GenMSAlg ()) /\ a2 by Def21
.= G1 by Th23 ; :: thesis: a "/\" G1 = G1
hence a "/\" G1 = G1 ; :: thesis: verum
end;
thus MSSubAlLattice U0 is upper-bounded :: thesis: verum
proof
reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;
reconsider G = GenMSAlg B as Element of MSSub U0 by Def19;
reconsider G1 = G as Element of () ;
take G1 ; :: according to LATTICES:def 14 :: thesis: for b1 being Element of the carrier of () holds
( G1 "\/" b1 = G1 & b1 "\/" G1 = G1 )

let a be Element of (); :: thesis: ( G1 "\/" a = G1 & a "\/" G1 = G1 )
reconsider a1 = a as Element of MSSub U0 ;
reconsider a2 = a1 as strict MSSubAlgebra of U0 by Def19;
thus G1 "\/" a = () "\/" a2 by Def20
.= G1 by Th25 ; :: thesis: a "\/" G1 = G1
hence a "\/" G1 = G1 ; :: thesis: verum
end;