defpred S₁[ Element of R, Element of R] means $1 in H . {$2};
consider RR being Relation of the carrier of R such that
A0: for x, y being Element of R holds
( [x,y] in RR iff S₁[x,y] ) from RELSET_1:sch 2();
take RR ; :: thesis: for x, y being Element of R holds
( [x,y] in RR iff x in H . {y} )
thus for x, y being Element of R holds
( [x,y] in RR iff x in H . {y} ) by A0; :: thesis: verum