let T be TopStruct ; :: thesis: for F being Subset-Family of T holds
( F is open iff COMPLEMENT F is closed )
let F be Subset-Family of T; :: thesis: ( F is open iff COMPLEMENT F is closed )
F = COMPLEMENT (COMPLEMENT F) ;
hence ( F is open iff COMPLEMENT F is closed ) by Th9; :: thesis: verum