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

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