for S, T being non empty RelStr
for A being Subset of S
for f being Function of S,T st f is isomorphic & ex_sup_of A,S holds
ex_sup_of f .: A,T