for T being 1-sorted
for P, Q being Subset of T st [#] T = P \/ Q & P misses Q holds
Q = ([#] T) \ P