reconsider C = UAStr(# A,(Opers (U0,A)) #) as strict Universal_Algebra by Th14;
for B being non empty Subset of U0 st B = the carrier of C holds
( the charact of C = Opers (U0,B) & B is opers_closed ) by A1;
hence UAStr(# A,(Opers (U0,A)) #) is strict SubAlgebra of U0 by Def7; :: thesis: verum