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

( 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 )

hence
G = H
by Th31; :: thesis: verum( 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;( P in G iff P ` in F ) by A1;

hence ( P in G iff P in H ) by A2; :: thesis: verum