let R1, R2 be Equivalence_Relation of (NonZero V); :: thesis: ( ( for x, y being object 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 object 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 object 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 object 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 object holds

( [x,y] in R1 iff [x,y] in R2 )

( [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 object 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 object 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 object 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 object holds

( [x,y] in R1 iff [x,y] in R2 )

proof

hence
R1 = R2
by RELAT_1:def 2; :: thesis: verum
let x, y be object ; :: thesis: ( [x,y] in R1 iff [x,y] in R2 )

end;A7: now :: thesis: ( [x,y] in R2 implies [x,y] in R1 )

assume A8:
[x,y] in R2
; :: thesis: [x,y] in R1

then A9: ex u, v being Element of V st

( x = u & y = v & are_Prop u,v ) by A6;

( x in NonZero V & y in NonZero V ) by A6, A8;

hence [x,y] in R1 by A5, A9; :: thesis: verum

end;then A9: ex u, v being Element of V st

( x = u & y = v & are_Prop u,v ) by A6;

( x in NonZero V & y in NonZero V ) by A6, A8;

hence [x,y] in R1 by A5, A9; :: thesis: verum

now :: thesis: ( [x,y] in R1 implies [x,y] in R2 )

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

then A11: ex u, v being Element of V st

( x = u & y = v & are_Prop u,v ) by A5;

( x in NonZero V & y in NonZero V ) by A5, A10;

hence [x,y] in R2 by A6, A11; :: thesis: verum

end;then A11: ex u, v being Element of V st

( x = u & y = v & are_Prop u,v ) by A5;

( x in NonZero V & y in NonZero V ) by A5, A10;

hence [x,y] in R2 by A6, A11; :: thesis: verum