defpred S_{1}[ 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_{1}[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

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

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