theorem Th4: :: CHAIN_1:4

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