let X, Y be set ; :: thesis: ( X is empty & X <> Y implies not Y is empty )
assume that
A1: X is empty and
A2: X <> Y ; :: thesis: not Y is empty
X = {} by A1, Lm1;
hence not Y is empty by A2, Lm1; :: thesis: verum