for X being set st X <> {} holds
ex x being object st x in X by Def1, Lm1;