:: A theory of partitions, { I } :: by Shunichi Kobayashi and Kui Jia :: :: Received October 5, 1998 :: Copyright (c) 1998-2012 Association of Mizar Users
uniqueness
for b1, b2 being Equivalence_Relation of Y st ( for x1, x2 being set holds ( [x1,x2]in b1 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 b2 iff ex A being Subset of Y st ( A in PA & x1 in A & x2 in A ) ) ) holds b1= b2