let T be 1-sorted ; :: thesis: for P being Subset of holds ([#] T) \ (([#] T) \ P) = P
let P be Subset of ; :: 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