for R, S being Relation st R,S are_isomorphic & R is finite holds
S is finite