let R1, R2 be Relation of X; :: thesis: ( ( for x, y being set holds
( x,y in R1 iff ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) ) ) ) & ( for x, y being set holds
( x,y in R2 iff ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) ) ) ) implies R1 = R2 )
assume that
A2: for x, y being set holds
( x,y in R1 iff ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) ) ) and
A3: for x, y being set holds
( x,y in R2 iff ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 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 ) )
reconsider xx = x, yy = y as set by TARSKI:1;
( [x,y] in R1 iff xx,yy in R1 ) ;
then ( [x,y] in R1 iff ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) ) ) by A2;
then ( [x,y] in R1 iff xx,yy in R2 ) by A3;
hence ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) ) ; :: thesis: verum