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