let S1 be OrderSortedSign; :: thesis: for U0 being non-empty OSAlgebra of S1
for B being OSSubset of U0 st B = the Sorts of U0 holds
Top (OSSubAlLattice U0) = GenOSAlg B
let U0 be non-empty OSAlgebra of S1; :: thesis: for B being OSSubset of U0 st B = the Sorts of U0 holds
Top (OSSubAlLattice U0) = GenOSAlg B
let B be OSSubset of U0; :: thesis: ( B = the Sorts of U0 implies Top (OSSubAlLattice U0) = GenOSAlg B )
reconsider G = GenOSAlg B as Element of OSSub U0 by Def15;
set L = OSSubAlLattice U0;
reconsider G1 = G as Element of (OSSubAlLattice U0) ;
assume A1: B = the Sorts of U0 ; :: thesis: Top (OSSubAlLattice U0) = GenOSAlg B

now

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 Def15;
thus G1 "\/" a = (GenOSAlg B) "\/"_os a2 by Def16
.= G1 by A1, Th43 ; :: thesis: a "\/" G1 = G1
hence a "\/" G1 = G1 ; :: thesis: verum

end;

hence Top (OSSubAlLattice U0) = GenOSAlg B by LATTICES:def 17; :: thesis: verum