let X be 1-sorted ; :: 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 SETFAM_1:def 7; :: 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 SETFAM_1:def 7; :: thesis: verum