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