theorem :: ORDERS_1:87

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