for U1, U2 being Universal_Algebra
for S1 being Subset of U1
for S2 being Subset of U2 st S1 = S2 holds
for o1 being operation of U1
for o2 being operation of U2 st o1 = o2 & S1 is_closed_on o1 holds
S2 is_closed_on o2