for T being 1-sorted
for P being Subset of T holds ([#] T) \ (([#] T) \ P) = P