let R be Relation; ( field R is finite implies R is finite )
assume
field R is finite
; R is finite
then reconsider A = field R as finite set ;
R c= [:A,A:]
proof
let y,
z be
object ;
RELAT_1:def 3 ( not [y,z] in R or [y,z] in [:A,A:] )
assume A1:
[y,z] in R
;
[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;
verum
end;
hence
R is finite
; verum