defpred S₁[ set , set ] 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 , such that
A1: for x, y being set 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 a', b', c', d' being Element of X such that
A2: [a,b] = [a',b'] and
A3: [c,d] = [c',d'] and
A4: ( [[a',b'],[c',d']] in R or [[a',b'],[d',c']] in R ) by A1;
c = c' by A3, ZFMISC_1:33;
hence ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) by A2, A3, A4, ZFMISC_1:33; :: 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