let T be non empty TopSpace; :: thesis: for U being open Subset of T
for A being Subset of T st A is closed holds
U \ A is open
let U be open Subset of T; :: thesis: for A being Subset of T st A is closed holds
U \ A is open
let A be Subset of T; :: thesis: ( A is closed implies U \ A is open )
A1: U /\ (([#] T) \ A) = U /\ (A `) ;
assume A is closed ; :: thesis: U \ A is open
hence U \ A is open by A1, SUBSET_1:13; :: thesis: verum