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