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

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