let f1, f2 be Equivalence_Relation of Y; :: thesis: ( ( for x1, x2 being object holds
( [x1,x2] in f1 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) ) & ( for x1, x2 being object holds
( [x1,x2] in f2 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) ) implies f1 = f2 )
assume that
A12: for x1, x2 being object holds
( [x1,x2] in f1 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) and
A13: for x1, x2 being object holds
( [x1,x2] in f2 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) ; :: thesis: f1 = f2
let x1, x2 be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x1,x2] in f1 or [x1,x2] in f2 ) & ( not [x1,x2] in f2 or [x1,x2] in f1 ) )
( [x1,x2] in f1 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) by A12;
hence ( ( not [x1,x2] in f1 or [x1,x2] in f2 ) & ( not [x1,x2] in f2 or [x1,x2] in f1 ) ) by A13; :: thesis: verum