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

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