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 )
proof
let x, y be object ; :: thesis: ( [x,y] in R1 iff [x,y] in R2 )
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;
now :: thesis: ( [x,y] in R1 implies [x,y] in R2 )
assume 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;
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