let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra over S

for B being MSSubset of U0 st B = the Sorts of U0 holds

Top (MSSubAlLattice U0) = GenMSAlg B

let U0 be non-empty MSAlgebra over S; :: thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds

Top (MSSubAlLattice U0) = GenMSAlg B

let B be MSSubset of U0; :: thesis: ( B = the Sorts of U0 implies Top (MSSubAlLattice U0) = GenMSAlg B )

reconsider G = GenMSAlg B as Element of MSSub U0 by Def19;

set L = MSSubAlLattice U0;

reconsider G1 = G as Element of (MSSubAlLattice U0) ;

assume A1: B = the Sorts of U0 ; :: thesis: Top (MSSubAlLattice U0) = GenMSAlg B

for B being MSSubset of U0 st B = the Sorts of U0 holds

Top (MSSubAlLattice U0) = GenMSAlg B

let U0 be non-empty MSAlgebra over S; :: thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds

Top (MSSubAlLattice U0) = GenMSAlg B

let B be MSSubset of U0; :: thesis: ( B = the Sorts of U0 implies Top (MSSubAlLattice U0) = GenMSAlg B )

reconsider G = GenMSAlg B as Element of MSSub U0 by Def19;

set L = MSSubAlLattice U0;

reconsider G1 = G as Element of (MSSubAlLattice U0) ;

assume A1: B = the Sorts of U0 ; :: thesis: Top (MSSubAlLattice U0) = GenMSAlg B

now :: thesis: for a being Element of (MSSubAlLattice U0) holds

( G1 "\/" a = G1 & a "\/" G1 = G1 )

hence
Top (MSSubAlLattice U0) = GenMSAlg B
by LATTICES:def 17; :: thesis: verum( 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 B) "\/" a2 by Def20

.= G1 by A1, Th25 ; :: thesis: a "\/" G1 = G1

hence a "\/" G1 = G1 ; :: thesis: verum

end;reconsider a1 = a as Element of MSSub U0 ;

reconsider a2 = a1 as strict MSSubAlgebra of U0 by Def19;

thus G1 "\/" a = (GenMSAlg B) "\/" a2 by Def20

.= G1 by A1, Th25 ; :: thesis: a "\/" G1 = G1

hence a "\/" G1 = G1 ; :: thesis: verum