theorem Th3: :: PRE_TOPC:3

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