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

end;

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