let S1 be OrderSortedSign; :: thesis: for U0 being non-empty OSAlgebra of S1 holds Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0)
let U0 be non-empty OSAlgebra of S1; :: thesis: Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0)
set C = OSConstants U0;
reconsider G = GenOSAlg (OSConstants U0) as Element of OSSub U0 by Def14;
set L = OSSubAlLattice U0;
reconsider G1 = G as Element of (OSSubAlLattice U0) ;

now :: thesis: for a being Element of (OSSubAlLattice U0) holds
( G1 "/\" a = G1 & a "/\" 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;

hence Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0) by LATTICES:def 16; :: thesis: verum