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

A1: UnSubAlLattice U0 is lower-bounded

A1: UnSubAlLattice U0 is lower-bounded

proof

UnSubAlLattice U0 is upper-bounded
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_{1} being Element of the carrier of (UnSubAlLattice U0) holds

( l1 "/\" b_{1} = l1 & b_{1} "/\" 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;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

( l1 "/\" b

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

proof

hence
UnSubAlLattice U0 is bounded
by A1; :: thesis: verum
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_{1} being Element of the carrier of (UnSubAlLattice U0) holds

( l1 "\/" b_{1} = l1 & b_{1} "\/" 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;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

( l1 "\/" b

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