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

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