defpred S₁[ set , set ] means $1 = $2;
consider R being Relation such that
A1: for x, y being set holds
( [x,y] in R iff ( x in X & y in X & S₁[x,y] ) ) from RELAT_1:sch 1();
take R ; :: thesis: for x, y being set holds
( [x,y] in R iff ( x in X & x = y ) )
let x, y be set ; :: thesis: ( [x,y] in R iff ( x in X & x = y ) )
thus ( [x,y] in R iff ( x in X & x = y ) ) by A1; :: thesis: verum