let G, H be Subset-Family of D; :: thesis: ( ( 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 ) ; :: thesis: G = H

now :: thesis: for P being Subset of D holds
( P in G iff P in H )

let P be Subset of D; :: thesis: ( P in G iff P in H )
( P in G iff P ` in F ) by A1;
hence ( P in G iff P in H ) by A2; :: thesis: verum

end;

hence G = H by Th31; :: thesis: verum