let T be non empty TopSpace; :: thesis: for A being Subset of T

for F being Subset-Family of T st F = {A} holds

( A is closed iff F is closed )

let A be Subset of T; :: thesis: for F being Subset-Family of T st F = {A} holds

( A is closed iff F is closed )

let F be Subset-Family of T; :: thesis: ( F = {A} implies ( A is closed iff F is closed ) )

assume A1: F = {A} ; :: thesis: ( A is closed iff F is closed )

A in F by A1, TARSKI:def 1;

hence A is closed by A2, TOPS_2:def 2; :: thesis: verum

for F being Subset-Family of T st F = {A} holds

( A is closed iff F is closed )

let A be Subset of T; :: thesis: for F being Subset-Family of T st F = {A} holds

( A is closed iff F is closed )

let F be Subset-Family of T; :: thesis: ( F = {A} implies ( A is closed iff F is closed ) )

assume A1: F = {A} ; :: thesis: ( A is closed iff F is closed )

hereby :: thesis: ( F is closed implies A is closed )

assume A2:
F is closed
; :: thesis: A is closed assume
A is closed
; :: thesis: F is closed

then for A being Subset of T st A in F holds

A is closed by A1, TARSKI:def 1;

hence F is closed by TOPS_2:def 2; :: thesis: verum

end;then for A being Subset of T st A in F holds

A is closed by A1, TARSKI:def 1;

hence F is closed by TOPS_2:def 2; :: thesis: verum

A in F by A1, TARSKI:def 1;

hence A is closed by A2, TOPS_2:def 2; :: thesis: verum