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 )
A1: B is OrderSortedSet of S1 by Def2;
assume A2: B = the Sorts of OU1 ; :: thesis: GenOSAlg B = OU1
then B is MSSubset of OU1 by PBOOLE:def 23;
then A3: B is OSSubset of OU1 by A1, Def2;
set W = GenOSAlg B;
A4: B is OSSubset of GenOSAlg B by Def13;
A5: GenOSAlg B is strict OSSubAlgebra of OU1 by A3, Def13;
the Sorts of OU1 c= the Sorts of (GenOSAlg B) by A2, A4, PBOOLE:def 23;
then OU1 is strict MSSubAlgebra of GenOSAlg B by MSUALG_2:9;
hence GenOSAlg B = OU1 by A5, MSUALG_2:8; :: thesis: verum