let X be set ; :: thesis: for F being Subset-Family of X
for P being Subset of X holds
( P ` in COMPLEMENT F iff P in F )
let F be Subset-Family of X; :: thesis: for P being Subset of X holds
( P ` in COMPLEMENT F iff P in F )
let P be Subset of X; :: thesis: ( P ` in COMPLEMENT F iff P in F )
P = (P `) ` ;
hence ( P ` in COMPLEMENT F iff P in F ) by Def7; :: thesis: verum