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:]
proof
let y, z be object ; :: according to RELAT_1:def 3 :: thesis: ( not [y,z] in R or [y,z] in [:A,A:] )
assume A1: [y,z] in R ; :: thesis: [y,z] in [:A,A:]
then A2: z in field R by RELAT_1:15;
y in field R by A1, RELAT_1:15;
hence [y,z] in [:A,A:] by A2, ZFMISC_1:87; :: thesis: verum
end;
hence R is finite ; :: thesis: verum