for A being Universal_Algebra
for B being Subset of A st B is opers_closed holds
Constants A c= B