let R be Relation; :: thesis: ( field R is finite implies R is finite )
assume field R is finite ; :: thesis: R is finite
then reconsider A = field R as finite set ;
R c= [:A,A:] by Lm6;
hence R is finite ; :: thesis: verum