given x, y being set such that A1: [x,y] in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ; :: thesis: contradiction
consider A being Subset of RAT+ such that
A2: [x,y] = A and
A3: for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) by A1;
A4: {x} in A by A2, TARSKI:def 2;
for r, s being Element of RAT+ st r in A & s <=' r holds
s in A by A3;
then consider r1, r2, r3 being Element of RAT+ such that
A5: ( r1 in A & r2 in A & r3 in A ) and
A6: ( r1 <> r2 & r2 <> r3 & r3 <> r1 ) by A4, ARYTM_3:82;
( ( r1 = {x,y} or r1 = {x} ) & ( r2 = {x,y} or r2 = {x} ) & ( r3 = {x,y} or r3 = {x} ) ) by A2, A5, TARSKI:def 2;
hence contradiction by A6; :: thesis: verum