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 = {} ) ) ) & ( for x, y being Element of X holds
( x,y in R2 iff ( x . O <> {} & y . O = {} ) ) ) implies R1 = R2 )
assume that
A3: for x, y being Element of X holds
( x,y in R1 iff ( x . O <> {} & y . O = {} ) ) and
A4: for x, y being Element of X holds
( x,y in R2 iff ( x . O <> {} & y . O = {} ) ) ; :: 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 ) )
reconsider xx = x, yy = y as set by TARSKI:1;
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 = {} ) by A3;
hence [x,y] in R2 by A4, MMLQUERY:def 1; :: 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 = {} ) by A4;
hence [x,y] in R1 by A3, MMLQUERY:def 1; :: thesis: verum