let X be non empty TopSpace; :: thesis: for A, B being Subset of X holds (A ` ) \ (B ` ) = B \ A
let A, B be Subset of X; :: thesis: (A ` ) \ (B ` ) = B \ A
(A ` ) \ (B ` ) = ([#] X) \ (A \/ (B ` )) by XBOOLE_1:41;
then (A ` ) \ (B ` ) = (A ` ) /\ ((B ` ) ` ) by XBOOLE_1:53;
hence (A ` ) \ (B ` ) = B \ A by SUBSET_1:32; :: thesis: verum