let X, Y be Subset of REAL ; :: thesis: ( X <> {} & Y <> {} implies X + Y <> {} )
assume X <> {} ; :: thesis: ( not Y <> {} or X + Y <> {} )
then consider x being Real such that
A1: x in X by SUBSET_1:10;
assume Y <> {} ; :: thesis: X + Y <> {}
then consider y being Real such that
A2: y in Y by SUBSET_1:10;
x + y in X + Y by A1, A2;
hence X + Y <> {} ; :: thesis: verum