thus ex D being Relation of the carrier of A st
for x, y being Element of A holds
( [x,y] in D iff S₁[x,y] ) from RELSET_1:sch 2(); :: thesis: verum