let S1 be OrderSortedSign; :: thesis: for OU0 being strict OSAlgebra of S1
for B being OSSubset of OU0 st B = the Sorts of OU0 holds
GenOSAlg B = OU0
let OU0 be strict OSAlgebra of S1; :: thesis: for B being OSSubset of OU0 st B = the Sorts of OU0 holds
GenOSAlg B = OU0
let B be OSSubset of OU0; :: thesis: ( B = the Sorts of OU0 implies GenOSAlg B = OU0 )
assume B = the Sorts of OU0 ; :: thesis: GenOSAlg B = OU0
then A1: GenMSAlg B = OU0 by MSUALG_2:22;
GenMSAlg B is strict MSSubAlgebra of GenOSAlg B by Th37, MSUALG_2:9;
hence GenOSAlg B = OU0 by A1, MSUALG_2:8; :: thesis: verum