defpred S₁[ object , object ] means ex x, y being Element of X st
( x = $1 & y = $2 & x \ y in A & y \ x in A );
consider P being Relation of X such that
A1: for x2, y2 being object holds
( [x2,y2] in P iff ( x2 in the carrier of X & y2 in the carrier of X & S₁[x2,y2] ) ) from RELSET_1:sch 1();
take P ; :: thesis: for x, y being Element of X holds
( [x,y] in P iff ( x \ y in A & y \ x in A ) )
let x2, y2 be Element of X; :: thesis: ( [x2,y2] in P iff ( x2 \ y2 in A & y2 \ x2 in A ) )
( [x2,y2] in P implies ex x1, y1 being Element of X st
( x1 = x2 & y1 = y2 & x1 \ y1 in A & y1 \ x1 in A ) ) by A1;
hence ( [x2,y2] in P implies ( x2 \ y2 in A & y2 \ x2 in A ) ) ; :: thesis: ( x2 \ y2 in A & y2 \ x2 in A implies [x2,y2] in P )
thus ( x2 \ y2 in A & y2 \ x2 in A implies [x2,y2] in P ) by A1; :: thesis: verum