let F, G be Subset-Family of D; :: thesis: ( ( for P being Subset of D holds

( P in F iff P ` in G ) ) implies for P being Subset of D holds

( P in G iff P ` in F ) )

assume A3: for P being Subset of D holds

( P in F iff P ` in G ) ; :: thesis: for P being Subset of D holds

( P in G iff P ` in F )

let P be Subset of D; :: thesis: ( P in G iff P ` in F )

(P `) ` = P ;

hence ( P in G iff P ` in F ) by A3; :: thesis: verum

( P in F iff P ` in G ) ) implies for P being Subset of D holds

( P in G iff P ` in F ) )

assume A3: for P being Subset of D holds

( P in F iff P ` in G ) ; :: thesis: for P being Subset of D holds

( P in G iff P ` in F )

let P be Subset of D; :: thesis: ( P in G iff P ` in F )

(P `) ` = P ;

hence ( P in G iff P ` in F ) by A3; :: thesis: verum