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: MSSubAlLattice U0 is bounded

set L = MSSubAlLattice U0;

thus MSSubAlLattice U0 is lower-bounded :: according to LATTICES:def 15 :: thesis: MSSubAlLattice U0 is upper-bounded

let U0 be non-empty MSAlgebra over S; :: thesis: MSSubAlLattice U0 is bounded

set L = MSSubAlLattice U0;

thus MSSubAlLattice U0 is lower-bounded :: according to LATTICES:def 15 :: thesis: MSSubAlLattice U0 is upper-bounded

proof

thus
MSSubAlLattice U0 is upper-bounded
:: thesis: verum
set C = Constants U0;

reconsider G = GenMSAlg (Constants U0) as Element of MSSub U0 by Def19;

reconsider G1 = G as Element of (MSSubAlLattice U0) ;

take G1 ; :: according to LATTICES:def 13 :: thesis: for b_{1} being Element of the carrier of (MSSubAlLattice U0) holds

( G1 "/\" b_{1} = G1 & b_{1} "/\" G1 = G1 )

let a be Element of (MSSubAlLattice U0); :: 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 (Constants U0)) /\ a2 by Def21

.= G1 by Th23 ; :: thesis: a "/\" G1 = G1

hence a "/\" G1 = G1 ; :: thesis: verum

end;reconsider G = GenMSAlg (Constants U0) as Element of MSSub U0 by Def19;

reconsider G1 = G as Element of (MSSubAlLattice U0) ;

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

( G1 "/\" b

let a be Element of (MSSubAlLattice U0); :: 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 (Constants U0)) /\ a2 by Def21

.= G1 by Th23 ; :: thesis: a "/\" G1 = G1

hence a "/\" G1 = G1 ; :: 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 (MSSubAlLattice U0) ;

take G1 ; :: according to LATTICES:def 14 :: thesis: for b_{1} being Element of the carrier of (MSSubAlLattice U0) holds

( G1 "\/" b_{1} = G1 & b_{1} "\/" G1 = G1 )

let a be Element of (MSSubAlLattice U0); :: 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 B) "\/" a2 by Def20

.= G1 by Th25 ; :: thesis: a "\/" G1 = G1

hence a "\/" G1 = G1 ; :: thesis: verum

end;reconsider G = GenMSAlg B as Element of MSSub U0 by Def19;

reconsider G1 = G as Element of (MSSubAlLattice U0) ;

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

( G1 "\/" b

let a be Element of (MSSubAlLattice U0); :: 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 B) "\/" a2 by Def20

.= G1 by Th25 ; :: thesis: a "\/" G1 = G1

hence a "\/" G1 = G1 ; :: thesis: verum