let A, B be Element of DEDEKIND_CUTS ; :: thesis: ( not A + B = {} or A = {} or B = {} )
assume A1: A + B = {} ; :: thesis: ( A = {} or B = {} )
assume A <> {} ; :: thesis: B = {}
then consider r0 being Element of RAT+ such that
A2: r0 in A by SUBSET_1:4;
assume B <> {} ; :: thesis: contradiction
then consider s0 being Element of RAT+ such that
A3: s0 in B by SUBSET_1:4;
r0 + s0 in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } by A2, A3;
hence contradiction by A1; :: thesis: verum