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

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