for TS being non empty set
for A, B being with_proper_subsets Subset-Family of TS holds A \/ B is with_proper_subsets