given x, y being object 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 ) ) }
; 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;
( {x} in A & ( for r, s being Element of RAT+ st r in A & s <=' r holds
s in A ) )
by A2, A3, TARSKI:def 2;
then consider r1, r2, r3 being Element of RAT+ such that
A4:
r1 in A
and
A5:
r2 in A
and
A6:
( r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 )
by ARYTM_3:75;
A7:
( r2 = {x,y} or r2 = {x} )
by A2, A5, TARSKI:def 2;
( r1 = {x,y} or r1 = {x} )
by A2, A4, TARSKI:def 2;
hence
contradiction
by A2, A6, A7, TARSKI:def 2; verum