let T be TopSpace; :: thesis: for A, B being Subset of T st A is open & B is closed holds
A \ B is open
let A, B be Subset of T; :: thesis: ( A is open & B is closed implies A \ B is open )
assume A1: ( A is open & B is closed ) ; :: thesis: A \ B is open
then ([#] T) \ B is open by PRE_TOPC:def 6;
then A /\ (([#] T) \ B) is open by A1, TOPS_1:38;
then A2: (A /\ ([#] T)) \ (A /\ B) is open by XBOOLE_1:50;
A /\ ([#] T) = A by XBOOLE_1:28;
hence A \ B is open by A2, XBOOLE_1:47; :: thesis: verum