let T be TopStruct ; :: thesis: for F being Subset-Family of T holds
( F is closed iff COMPLEMENT F is open )
let F be Subset-Family of T; :: thesis: ( F is closed iff COMPLEMENT F is open )
thus ( F is closed implies COMPLEMENT F is open ) :: thesis: ( COMPLEMENT F is open implies F is closed )

proof

assume A1: F is closed ; :: thesis: COMPLEMENT F is open
let P be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( P in COMPLEMENT F implies P is open )
assume P in COMPLEMENT F ; :: thesis: P is open
then P ` in F by SETFAM_1:def 8;
then P ` is closed by A1, Def2;
hence P is open by TOPS_1:30; :: thesis: verum

end;

assume A2: COMPLEMENT F is open ; :: thesis: F is closed
let P be Subset of T; :: according to TOPS_2:def 2 :: thesis: ( P in F implies P is closed )
assume A3: P in F ; :: thesis: P is closed
(P ` ) ` = P ;
then P ` in COMPLEMENT F by A3, SETFAM_1:def 8;
then P ` is open by A2, Def1;
hence P is closed by TOPS_1:29; :: thesis: verum