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:21;
GenMSAlg B is strict MSSubAlgebra of GenOSAlg B by Th32, MSUALG_2:8;
hence GenOSAlg B = OU0 by A1, MSUALG_2:7; :: thesis: verum