let X be set ; :: thesis: for R being Relation st field R c= X holds
R is Relation of X
let R be Relation; :: thesis: ( field R c= X implies R is Relation of X )
assume A1: field R c= X ; :: thesis: R is Relation of X
let x, y be set ; :: according to RELSET_1:def 1,RELAT_1:def 3 :: thesis: ( not [x,y] in R or [x,y] in [:X,X:] )
assume [x,y] in R ; :: thesis: [x,y] in [:X,X:]
then ( x in field R & y in field R ) by RELAT_1:30;
hence [x,y] in [:X,X:] by A1, ZFMISC_1:def 2; :: thesis: verum