let T be 1-sorted ; :: thesis: for P being Subset of T holds ([#] T) \ (([#] T) \ P) = P
let P be Subset of T; :: thesis: ([#] T) \ (([#] T) \ P) = P
([#] T) \ (([#] T) \ P) = P /\ ([#] T) by XBOOLE_1:48;
hence ([#] T) \ (([#] T) \ P) = P by XBOOLE_1:28; :: thesis: verum