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 that
A1: A is open and
A2: B is closed ; :: thesis: A \ B is open
([#] T) \ B is open by A2, PRE_TOPC:def 3;
then A /\ (([#] T) \ B) is open by A1, TOPS_1:11;
then A3: (A /\ ([#] T)) \ (A /\ B) is open by XBOOLE_1:50;
A /\ ([#] T) = A by XBOOLE_1:28;
hence A \ B is open by A3, XBOOLE_1:47; :: thesis: verum