let A be Subset of RAT+ ; :: thesis:
given t being Element of RAT+ such that A1: ( t in A & t <> {} ) ; :: thesis:
assume A2: for r, s being Element of RAT+ st r in A & s <=' r holds
s in A ; :: thesis:
consider x being Element of RAT+ such that
A3: t = x + x by ARYTM_3:66;
consider y being Element of RAT+ such that
A4: x = y + y by ARYTM_3:66;
consider w being Element of RAT+ such that
A5: y = w + w by ARYTM_3:66;
take {} ; :: thesis:
take w ; :: thesis:
take y ; :: thesis:
take x ; :: thesis:
take t ; :: thesis:
A6: ( {} <=' t & x <=' t ) by A3, ARYTM_3:71, ARYTM_3:def 13;
A7: ( y <=' x & w <=' y ) by A4, A5, ARYTM_3:def 13;
then A8: y <=' t by A6, ARYTM_3:74;
w <=' x by A7, ARYTM_3:74;
hence ( {} in A & w in A & y in A & x in A & t in A ) by A1, A2, A6, A7, ARYTM_3:74; :: thesis:
A9: {} <> x by A1, A3, ARYTM_3:56;
then A10: {} <> y by A4, ARYTM_3:56;
A11: x <> t

proof

assume x = t ; :: thesis:
then t + {} = t + t by A3, ARYTM_3:56;
hence contradiction by A1, ARYTM_3:69; :: thesis:

end;

A12: y <> x

proof

assume y = x ; :: thesis:
then x + {} = x + x by A4, ARYTM_3:56;
hence contradiction by A9, ARYTM_3:69; :: thesis:

end;

w <> y

proof

assume w = y ; :: thesis:
then y + {} = y + y by A5, ARYTM_3:56;
hence contradiction by A10, ARYTM_3:69; :: thesis:

end;

hence ( {} <> w & {} <> y & {} <> x & {} <> t & w <> y & w <> x & w <> t & y <> x & y <> t & x <> t ) by A1, A3, A4, A5, A6, A7, A8, A11, A12, ARYTM_3:56, ARYTM_3:73; :: thesis: