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 )