let T be TopStruct ; :: thesis: for A being Subset of T holds
( A is open iff ([#] T) \ A is closed )
let A be Subset of T; :: thesis: ( A is open iff ([#] T) \ A is closed )
thus ( A is open implies ([#] T) \ A is closed ) :: thesis: ( ([#] T) \ A is closed implies A is open )

proof

assume A is open ; :: thesis: ([#] T) \ A is closed
then ([#] T) \ (([#] T) \ A) is open by PRE_TOPC:3;
hence ([#] T) \ A is closed by PRE_TOPC:def 3; :: thesis: verum

end;

assume ([#] T) \ A is closed ; :: thesis: A is open
then ([#] T) \ (([#] T) \ A) is open by PRE_TOPC:def 3;
hence A is open by PRE_TOPC:3; :: thesis: verum