let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for OU1 being strict OSSubAlgebra of OU0
for B being OSSubset of OU0 st B = the Sorts of OU1 holds
GenOSAlg B = OU1
let OU0 be OSAlgebra of S1; :: thesis: for OU1 being strict OSSubAlgebra of OU0
for B being OSSubset of OU0 st B = the Sorts of OU1 holds
GenOSAlg B = OU1
let OU1 be strict OSSubAlgebra of OU0; :: thesis: for B being OSSubset of OU0 st B = the Sorts of OU1 holds
GenOSAlg B = OU1
let B be OSSubset of OU0; :: thesis: ( B = the Sorts of OU1 implies GenOSAlg B = OU1 )
set W = GenOSAlg B;
assume A1: B = the Sorts of OU1 ; :: thesis: GenOSAlg B = OU1
then A2: B is MSSubset of OU1 by PBOOLE:def 18;
B is OSSubset of GenOSAlg B by Def12;
then the Sorts of OU1 c= the Sorts of (GenOSAlg B) by A1, PBOOLE:def 18;
then A3: OU1 is strict MSSubAlgebra of GenOSAlg B by MSUALG_2:8;
B is OrderSortedSet of S1 by Def2;
then B is OSSubset of OU1 by A2, Def2;
then GenOSAlg B is strict OSSubAlgebra of OU1 by Def12;
hence GenOSAlg B = OU1 by A3, MSUALG_2:7; :: thesis: verum