let A be Subset of RAT+; :: thesis:
given t being Element of RAT+ such that A1: t in A and
A2: t <> {} ; :: thesis:
assume A3: 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
A4: t = x + x by ARYTM_3:60;
consider y being Element of RAT+ such that
A5: x = y + y by ARYTM_3:60;
consider w being Element of RAT+ such that
A6: y = w + w by ARYTM_3:60;
take {} ; :: thesis:
take w ; :: thesis:
take y ; :: thesis:
take x ; :: thesis:
take t ; :: thesis:
A7: {} <=' t by ARYTM_3:64;
A8: x <=' t by A4;
A9: y <=' x by A5;
A10: w <=' y by A6;
A11: y <=' t by A8, A9, ARYTM_3:67;
w <=' x by A9, A10, ARYTM_3:67;
hence ( {} in A & w in A & y in A & x in A & t in A ) by A1, A3, A7, A8, A9, ARYTM_3:67; :: thesis:
A12: {} <> x by A2, A4, ARYTM_3:50;
then A13: {} <> y by A5, ARYTM_3:50;
A14: x <> t

proof

assume x = t ; :: thesis:
then t + {} = t + t by A4, ARYTM_3:50;
hence contradiction by A2, ARYTM_3:62; :: thesis:

end;

A15: y <> x

proof

assume y = x ; :: thesis:
then x + {} = x + x by A5, ARYTM_3:50;
hence contradiction by A12, ARYTM_3:62; :: thesis:

end;

w <> y

proof

assume w = y ; :: thesis:
then y + {} = y + y by A6, ARYTM_3:50;
hence contradiction by A13, ARYTM_3:62; :: thesis:

end;

hence ( {} <> w & {} <> y & {} <> x & {} <> t & w <> y & w <> x & w <> t & y <> x & y <> t & x <> t ) by A2, A4, A5, A6, A8, A9, A10, A11, A14, A15, ARYTM_3:50, ARYTM_3:66; :: thesis: