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 open iff F is open )
let A be Subset of T; :: thesis: for F being Subset-Family of T st F = {A} holds
( A is open iff F is open )
let F be Subset-Family of T; :: thesis: ( F = {A} implies ( A is open iff F is open ) )
assume A1: F = {A} ; :: thesis: ( A is open iff F is open )

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

assume A is open ; :: thesis: F is open
then for A being Subset of T st A in F holds
A is open by A1, TARSKI:def 1;
hence F is open by TOPS_2:def 1; :: thesis: verum

end;

assume A2: F is open ; :: thesis: A is open
A in F by A1, TARSKI:def 1;
hence A is open by A2, TOPS_2:def 1; :: thesis: verum