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, MEMBER_1:46;
hence X ++ Y <> {} ; :: thesis: verum