let R, S be Relation; :: thesis: ( R,S are_isomorphic & R is finite implies S is finite )
given F being Function such that A1: F is_isomorphism_of R,S ; :: according to WELLORD1:def 8 :: thesis: ( not R is finite or S is finite )
assume R is finite ; :: thesis: S is finite
then field R is finite ;
then dom F is finite by A1;
then rng F is finite by FINSET_1:8;
then field S is finite by A1;
hence S is finite ; :: thesis: verum