defpred S₁[ object , object ] means ( Im (O,$1) <> {} & Im (O,$2) = {} );
consider R being Relation such that
A1: for x, y being object holds
( [x,y] in R iff ( x in X & y in X & S₁[x,y] ) ) from RELAT_1:sch 1();
R c= [:X,X:]

proof

let x, y be object ; :: according to 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 X & y in X ) by A1;
hence [x,y] in [:X,X:] by ZFMISC_1:87; :: thesis: verum

end;

then reconsider R = R as Relation of X ;
take R ; :: thesis: for x, y being Element of X holds
( x,y in R iff ( x . O <> {} & y . O = {} ) )
let x, y be Element of X; :: thesis: ( x,y in R iff ( x . O <> {} & y . O = {} ) )
A2: ( x . O <> {} iff x in dom O ) by RELAT_1:170;
thus ( x,y in R iff ( x . O <> {} & y . O = {} ) ) by A1, A2; :: thesis: verum