let U0 be strict with_const_op Universal_Algebra; :: thesis: UnSubAlLattice U0 is bounded
A1: UnSubAlLattice U0 is lower-bounded

proof

reconsider U11 = Constants U0 as Subset of U0 ;
reconsider U2 = GenUnivAlg (Constants U0) as strict SubAlgebra of U0 ;
reconsider l1 = GenUnivAlg (Constants U0) as Element of (UnSubAlLattice U0) by UNIALG_2:def 14;
take l1 ; :: according to LATTICES:def 13 :: thesis: for b₁ being Element of the carrier of (UnSubAlLattice U0) holds
( l1 "/\" b₁ = l1 & b₁ "/\" l1 = l1 )
let l2 be Element of (UnSubAlLattice U0); :: thesis: ( l1 "/\" l2 = l1 & l2 "/\" l1 = l1 )
reconsider U1 = l2 as strict SubAlgebra of U0 by UNIALG_2:def 14;
reconsider U21 = the carrier of U1 as Subset of U0 by UNIALG_2:def 7;
reconsider U3 = U11 \/ U21 as non empty Subset of U0 ;
Constants U0 is Subset of U1 by UNIALG_2:16;
then GenUnivAlg U3 = U1 by UNIALG_2:19, XBOOLE_1:12;
then U2 "\/" U1 = U1 by UNIALG_2:20;
then l1 "\/" l2 = l2 by UNIALG_2:def 15;
then A2: l1 [= l2 ;
hence l1 "/\" l2 = l1 by LATTICES:4; :: thesis: l2 "/\" l1 = l1
thus l2 "/\" l1 = l1 by A2, LATTICES:4; :: thesis: verum

end;

UnSubAlLattice U0 is upper-bounded

proof

U0 is strict SubAlgebra of U0 by UNIALG_2:8;
then reconsider l1 = U0 as Element of (UnSubAlLattice U0) by UNIALG_2:def 14;
reconsider U1 = l1 as strict SubAlgebra of U0 by UNIALG_2:8;
take l1 ; :: according to LATTICES:def 14 :: thesis: for b₁ being Element of the carrier of (UnSubAlLattice U0) holds
( l1 "\/" b₁ = l1 & b₁ "\/" l1 = l1 )
let l2 be Element of (UnSubAlLattice U0); :: thesis: ( l1 "\/" l2 = l1 & l2 "\/" l1 = l1 )
reconsider U2 = l2 as strict SubAlgebra of U0 by UNIALG_2:def 14;
reconsider U11 = the carrier of U1 as Subset of U0 by UNIALG_2:def 7;
reconsider U21 = the carrier of U2 as Subset of U0 by UNIALG_2:def 7;
reconsider H = U11 \/ U21 as non empty Subset of U0 ;
A3: H = the carrier of U1 by XBOOLE_1:12;
thus l1 "\/" l2 = U1 "\/" U2 by UNIALG_2:def 15
.= GenUnivAlg ([#] the carrier of U1) by A3, UNIALG_2:def 13
.= l1 by UNIALG_2:18 ; :: thesis: l2 "\/" l1 = l1
hence l2 "\/" l1 = l1 ; :: thesis: verum

end;

hence UnSubAlLattice U0 is bounded by A1; :: thesis: verum