let f1, f2 be Equivalence_Relation of Y; :: thesis: ( ( for x1, x2 being set 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 set 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
A1: for x1, x2 being set holds
( [x1,x2] in f1 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) and
A2: for x1, x2 being set 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 set ; :: 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 ) )
A3: ( [x1,x2] in f1 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) by A1;
thus ( ( not [x1,x2] in f1 or [x1,x2] in f2 ) & ( not [x1,x2] in f2 or [x1,x2] in f1 ) ) by A2, A3; :: thesis: verum