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

proof

reconsider l1 = GenUnivAlg (Constants U0) as Element of (UnSubAlLattice U0) by UNIALG_2:def 15;
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 15;
A2: Constants U0 is Subset of U1 by UNIALG_2:19;
reconsider U2 = GenUnivAlg (Constants U0) as strict SubAlgebra of U0 ;
reconsider U11 = Constants U0 as Subset of U0 ;
reconsider U21 = the carrier of U1 as Subset of U0 by UNIALG_2:def 8;
reconsider U3 = U11 \/ U21 as non empty Subset of U0 ;
GenUnivAlg U3 = U1 by A2, UNIALG_2:22, XBOOLE_1:12;
then U2 "\/" U1 = U1 by UNIALG_2:23;
then l1 "\/" l2 = l2 by UNIALG_2:def 16;
then A3: l1 [= l2 by LATTICES:22;
hence l1 "/\" l2 = l1 by LATTICES:21; :: thesis: l2 "/\" l1 = l1
thus l2 "/\" l1 = l1 by A3, LATTICES:21; :: thesis: verum

end;

UnSubAlLattice U0 is upper-bounded

proof

U0 is strict SubAlgebra of U0 by UNIALG_2:11;
then reconsider l1 = U0 as Element of (UnSubAlLattice U0) by UNIALG_2:def 15;
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 U1 = l1 as strict SubAlgebra of U0 by UNIALG_2:11;
reconsider U2 = l2 as strict SubAlgebra of U0 by UNIALG_2:def 15;
reconsider U11 = the carrier of U1 as Subset of U0 by UNIALG_2:def 8;
reconsider U21 = the carrier of U2 as Subset of U0 by UNIALG_2:def 8;
reconsider H = U11 \/ U21 as non empty Subset of U0 ;
A4: H = the carrier of U1 by XBOOLE_1:12;
thus l1 "\/" l2 = U1 "\/" U2 by UNIALG_2:def 16
.= GenUnivAlg ([#] the carrier of U1) by A4, UNIALG_2:def 14
.= l1 by UNIALG_2:21 ; :: thesis: l2 "\/" l1 = l1
hence l2 "\/" l1 = l1 ; :: thesis: verum

end;

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