let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra over S holds Bottom (MSSubAlLattice U0) = GenMSAlg (Constants U0)
let U0 be non-empty MSAlgebra over S; :: thesis: Bottom (MSSubAlLattice U0) = GenMSAlg (Constants U0)
set C = Constants U0;
reconsider G = GenMSAlg (Constants U0) as Element of MSSub U0 by Def19;
set L = MSSubAlLattice U0;
reconsider G1 = G as Element of (MSSubAlLattice U0) ;
now :: thesis: for a being Element of (MSSubAlLattice U0) holds
( G1 "/\" a = G1 & a "/\" 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;
hence Bottom (MSSubAlLattice U0) = GenMSAlg (Constants U0) by LATTICES:def 16; :: thesis: verum