let T be non empty TopSpace; :: thesis: for G, F being Subset of T st G is open & F is closed holds

F \ G is closed

let G, F be Subset of T; :: thesis: ( G is open & F is closed implies F \ G is closed )

assume A1: ( G is open & F is closed ) ; :: thesis: F \ G is closed

F \ G = F /\ (G `) by SUBSET_1:13;

hence F \ G is closed by A1; :: thesis: verum

F \ G is closed

let G, F be Subset of T; :: thesis: ( G is open & F is closed implies F \ G is closed )

assume A1: ( G is open & F is closed ) ; :: thesis: F \ G is closed

F \ G = F /\ (G `) by SUBSET_1:13;

hence F \ G is closed by A1; :: thesis: verum