theorem Th86: :: ORDERS_1:86

for R being Relation st field R is finite holds
R is finite