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 7;
then P ` is closed by A1;
hence P is open by TOPS_1:4; :: 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 7;
then P ` is open by A2;
hence P is closed ; :: thesis: verum