for A being Subset of RAT+ st ex t being Element of RAT+ st ( t in A & t <>{} ) & ( for r, s being Element of RAT+ st r in A & s <=' r holds s in A ) holds ex r1, r2, r3, r4, r5 being Element of RAT+ st ( r1 in A & r2 in A & r3 in A & r4 in A & r5 in A & r1 <> r2 & r1 <> r3 & r1 <> r4 & r1 <> r5 & r2 <> r3 & r2 <> r4 & r2 <> r5 & r3 <> r4 & r3 <> r5 & r4 <> r5 )