reconsider E = MSAlgebra(# A,(Opers U0,A) #) as MSAlgebra of 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 Def10; :: thesis: verum