for X, y being set st X is trivial & not X \/ {y} is trivial holds
ex x being object st X = {x}