let R1, R2 be Relation of X; :: 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 ) ) ) ) ) & ( for x, y being Element of X holds
( x,y in R2 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 ) ) ) ) ) implies R1 = R2 )
assume that
A3: 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 ) ) ) ) and
A4: for x, y being Element of X holds
( x,y in R2 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 ) ) ) ) ; :: thesis: R1 = R2
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) )
thus ( [x,y] in R1 implies [x,y] in R2 ) :: thesis: ( not [x,y] in R2 or [x,y] in R1 )

proof

assume A5: [x,y] in R1 ; :: thesis: [x,y] in R2
then reconsider x = x, y = y as Element of X by ZFMISC_1:87;
x,y in R1 by A5;
then ( 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 ) ) ) by A3;
then x,y in R2 by A4;
hence [x,y] in R2 ; :: thesis: verum

end;

assume A6: [x,y] in R2 ; :: thesis: [x,y] in R1
then reconsider x = x, y = y as Element of X by ZFMISC_1:87;
x,y in R2 by A6;
then ( 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 ) ) ) by A4;
then x,y in R1 by A3;
hence [x,y] in R1 ; :: thesis: verum