reconsider E = MSAlgebra(# A,(Opers (U0,A)) #) as MSAlgebra over S ;
for B being MSSubset of U0 st B = the Sorts of E holds
( B is opers_closed & the Charact of E = Opers (U0,B) ) by A1;
hence MSAlgebra(# A,(Opers (U0,A)) #) is strict MSSubAlgebra of U0 by Def9; :: thesis: verum