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