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 )

then ([#] T) \ (([#] T) \ A) is open by PRE_TOPC:def 3;

hence A is open by PRE_TOPC:3; :: thesis: verum

( 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
([#] T) \ A is closed
; :: thesis: A is open
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;then ([#] T) \ (([#] T) \ A) is open by PRE_TOPC:3;

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

then ([#] T) \ (([#] T) \ A) is open by PRE_TOPC:def 3;

hence A is open by PRE_TOPC:3; :: thesis: verum