let G, H be Subset-Family of D; ( ( for P being Subset of D holds
( P in G iff P ` in F ) ) & ( for P being Subset of D holds
( P in H iff P ` in F ) ) implies G = H )
assume that
A1:
for P being Subset of D holds
( P in G iff P ` in F )
and
A2:
for P being Subset of D holds
( P in H iff P ` in F )
; G = H
hence
G = H
by Th31; verum