theorem Th31: :: SETFAM_1:31

for D being set
for F, G being Subset-Family of D st ( for P being Subset of D holds
( P in F iff P in G ) ) holds
F = G