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