let X be TopStruct ; :: thesis: for F being Subset-Family of X holds
( F is closed iff F c= COMPLEMENT the topology of X )
let F be Subset-Family of X; :: thesis: ( F is closed iff F c= COMPLEMENT the topology of X )
thus ( F is closed implies F c= COMPLEMENT the topology of X ) :: thesis: ( F c= COMPLEMENT the topology of X implies F is closed )

proof

assume A1: F is closed ; :: thesis: F c= COMPLEMENT the topology of X
let A be set ; :: according to TARSKI:def 3 :: thesis: ( not A in F or A in COMPLEMENT the topology of X )
assume A2: A in F ; :: thesis: A in COMPLEMENT the topology of X
then reconsider A = A as Subset of X ;
A is closed by A1, A2, Def2;
then A ` is open by TOPS_1:3;
then A ` in the topology of X by PRE_TOPC:def 2;
hence A in COMPLEMENT the topology of X by SETFAM_1:def 7; :: thesis: verum

end;

assume A3: F c= COMPLEMENT the topology of X ; :: thesis: F is closed
let A be Subset of X; :: according to TOPS_2:def 2 :: thesis: ( A in F implies A is closed )
assume A in F ; :: thesis: A is closed
then A ` in the topology of X by A3, SETFAM_1:def 7;
then A ` is open by PRE_TOPC:def 2;
hence A is closed by TOPS_1:3; :: thesis: verum