let S1 be OrderSortedSign; :: thesis: for U0 being non-empty OSAlgebra of S1 holds OSSubAlLattice U0 is bounded
let U0 be non-empty OSAlgebra of S1; :: thesis: OSSubAlLattice U0 is bounded
set L = OSSubAlLattice U0;
thus OSSubAlLattice U0 is lower-bounded :: according to LATTICES:def 15 :: thesis: OSSubAlLattice U0 is upper-bounded

proof

set C = OSConstants U0;
reconsider G = GenOSAlg (OSConstants U0) as Element of OSSub U0 by Def14;
reconsider G1 = G as Element of (OSSubAlLattice U0) ;
take G1 ; :: according to LATTICES:def 13 :: thesis: for b₁ being Element of the carrier of (OSSubAlLattice U0) holds
( G1 "/\" b₁ = G1 & b₁ "/\" G1 = G1 )
let a be Element of (OSSubAlLattice U0); :: thesis: ( G1 "/\" a = G1 & a "/\" G1 = G1 )
reconsider a1 = a as Element of OSSub U0 ;
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14;
thus G1 "/\" a = (GenOSAlg (OSConstants U0)) /\ a2 by Def16
.= G1 by Th36 ; :: thesis: a "/\" G1 = G1
hence a "/\" G1 = G1 ; :: thesis: verum

end;

thus OSSubAlLattice U0 is upper-bounded :: thesis: verum

proof

reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;
the Sorts of U0 is OrderSortedSet of S1 by OSALG_1:17;
then reconsider B = B as OSSubset of U0 by Def2;
reconsider G = GenOSAlg B as Element of OSSub U0 by Def14;
reconsider G1 = G as Element of (OSSubAlLattice U0) ;
take G1 ; :: according to LATTICES:def 14 :: thesis: for b₁ being Element of the carrier of (OSSubAlLattice U0) holds
( G1 "\/" b₁ = G1 & b₁ "\/" G1 = G1 )
let a be Element of (OSSubAlLattice U0); :: thesis: ( G1 "\/" a = G1 & a "\/" G1 = G1 )
reconsider a1 = a as Element of OSSub U0 ;
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14;
thus G1 "\/" a = (GenOSAlg B) "\/"_os a2 by Def15
.= G1 by Th38 ; :: thesis: a "\/" G1 = G1
hence a "\/" G1 = G1 ; :: thesis: verum

end;