for R being Relation st dom R is finite & rng R is finite holds
R is finite