for TS being 1-sorted
for K, Q being Subset of TS st K ` = Q ` holds
K = Q by SUBSET_1:42;