for S being non empty non void ManySortedSign
for U0, U1 being non-empty MSAlgebra over S
for E being EqualSet of S st U0,U1 are_isomorphic & U0 |= E holds
U1 |= E by Th33;