:: Families of Subsets, Subspaces and Mappings in Topological Spaces :: by Agata Darmochwa{\l} :: :: Received June 21, 1989 :: Copyright (c) 1990-2012 Association of Mizar Users
uniqueness
for b1, b2 being Subset-Family of (T | P) st ( for Q being Subset of (T | P) holds ( Q in b1 iff ex R being Subset of T st ( R in F & R /\ P = Q ) ) ) & ( for Q being Subset of (T | P) holds ( Q in b2 iff ex R being Subset of T st ( R in F & R /\ P = Q ) ) ) holds b1= b2
:: A FAMILY OF SETS IN TOPOLOGICAL SPACES
::