defpred S₁[ object , object ] means ex x, y being Element of X st
( $1 = x & $2 = y & x . O <> {} & ( y . O = {} or ( y . O <> {} & (order ((x . O),R)) /. 0,(order ((y . O),R)) /. 0 in R & (order ((x . O),R)) /. 0 <> (order ((y . O),R)) /. 0 ) ) );
consider R1 being Relation such that
A1: for x, y being object holds
( [x,y] in R1 iff ( x in X & y in X & S₁[x,y] ) ) from RELAT_1:sch 1();
R1 c= [:X,X:]

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in R1 or [x,y] in [:X,X:] )
assume [x,y] in R1 ; :: thesis: [x,y] in [:X,X:]
then ( x in X & y in X ) by A1;
hence [x,y] in [:X,X:] by ZFMISC_1:87; :: thesis: verum

end;

then reconsider R1 = R1 as Relation of X ;
take R1 ; :: thesis: for x, y being Element of X holds
( x,y in R1 iff ( x . O <> {} & ( y . O = {} or ( y . O <> {} & (order ((x . O),R)) /. 0,(order ((y . O),R)) /. 0 in R & (order ((x . O),R)) /. 0 <> (order ((y . O),R)) /. 0 ) ) ) )
let x, y be Element of X; :: thesis: ( x,y in R1 iff ( x . O <> {} & ( y . O = {} or ( y . O <> {} & (order ((x . O),R)) /. 0,(order ((y . O),R)) /. 0 in R & (order ((x . O),R)) /. 0 <> (order ((y . O),R)) /. 0 ) ) ) )
A2: ( x . O <> {} implies x in dom O ) by RELAT_1:170;

hereby :: thesis: ( x . O <> {} & ( y . O = {} or ( y . O <> {} & (order ((x . O),R)) /. 0,(order ((y . O),R)) /. 0 in R & (order ((x . O),R)) /. 0 <> (order ((y . O),R)) /. 0 ) ) implies x,y in R1 )

assume x,y in R1 ; :: thesis: ( x . O <> {} & ( y . O = {} or ( y . O <> {} & (order ((x . O),R)) /. 0,(order ((y . O),R)) /. 0 in R & (order ((x . O),R)) /. 0 <> (order ((y . O),R)) /. 0 ) ) )
then S₁[x,y] by A1;
hence ( x . O <> {} & ( y . O = {} or ( y . O <> {} & (order ((x . O),R)) /. 0,(order ((y . O),R)) /. 0 in R & (order ((x . O),R)) /. 0 <> (order ((y . O),R)) /. 0 ) ) ) ; :: thesis: verum

end;

assume ( x . O <> {} & ( y . O = {} or ( y . O <> {} & (order ((x . O),R)) /. 0,(order ((y . O),R)) /. 0 in R & (order ((x . O),R)) /. 0 <> (order ((y . O),R)) /. 0 ) ) ) ; :: thesis: x,y in R1
hence x,y in R1 by A1, A2; :: thesis: verum