theorem :: SEQ_4:123

for X, Y being Subset of REAL st X <> {} & Y <> {} holds
X ++ Y <> {} ;