let X be non empty 1-sorted ; :: 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:13; :: thesis: verum