reconsider C = UAStr(# A,(Opers (U0,A)) #) as strict Universal_Algebra by Th17;
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 Def8; :: thesis: verum