let R1, R2 be Equivalence_Relation of (NonZero V); :: thesis: ( ( for x, y being set holds
( [x,y] in R1 iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) ) ) & ( for x, y being set holds
( [x,y] in R2 iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) ) ) implies R1 = R2 )
assume that
A5: for x, y being set holds
( [x,y] in R1 iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) ) and
A6: for x, y being set holds
( [x,y] in R2 iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) ) ; :: thesis: R1 = R2
for x, y being set holds
( [x,y] in R1 iff [x,y] in R2 )

proof

let x, y be set ; :: thesis: ( [x,y] in R1 iff [x,y] in R2 )

A7: now

assume [x,y] in R1 ; :: thesis: [x,y] in R2
then ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) by A5;
hence [x,y] in R2 by A6; :: thesis: verum

end;

now

assume [x,y] in R2 ; :: thesis: [x,y] in R1
then ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) by A6;
hence [x,y] in R1 by A5; :: thesis: verum

end;

hence ( [x,y] in R1 iff [x,y] in R2 ) by A7; :: thesis: verum

end;

hence R1 = R2 by RELAT_1:def 2; :: thesis: verum