defpred S₁[ object , object ] means ex a, b, c, d being Element of X st
( $1 = [a,b] & $2 = [c,d] & ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) );
set XX = [:X,X:];
consider P being Relation of [:X,X:],[:X,X:] such that
A1: for x, y being object holds
( [x,y] in P iff ( x in [:X,X:] & y in [:X,X:] & S₁[x,y] ) ) from RELSET_1:sch 1();
take P ; :: thesis: for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in P iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) )
let a, b, c, d be Element of X; :: thesis: ( [[a,b],[c,d]] in P iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) )
( not [[a,b],[c,d]] in P or [[a,b],[c,d]] in R or [[a,b],[d,c]] in R )

proof

assume [[a,b],[c,d]] in P ; :: thesis: ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R )
then consider a9, b9, c9, d9 being Element of X such that
A2: [a,b] = [a9,b9] and
A3: [c,d] = [c9,d9] and
A4: ( [[a9,b9],[c9,d9]] in R or [[a9,b9],[d9,c9]] in R ) by A1;
c = c9 by A3, XTUPLE_0:1;
hence ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) by A2, A3, A4, XTUPLE_0:1; :: thesis: verum

end;

hence ( [[a,b],[c,d]] in P iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) by A1; :: thesis: verum