set IR = { A where A is Subset of : 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 ) ) } ;
let x, y be set ; :: according to ORDINAL1:def 9 :: thesis: ( not x in { A where A is Subset of : 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 ) ) } or not y in { A where A is Subset of : 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 ) ) } or not R5(x,y) )
assume x in { A where A is Subset of : 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: ( not y in { A where A is Subset of : 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 ) ) } or not R5(x,y) )
then A1: ex A' being Subset of st
( x = A' & ( 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 ) ) ) ) ;
assume y in { A where A is Subset of : 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: R5(x,y)
then A2: ex B' being Subset of st
( y = B' & ( for r being Element of RAT+ st r in B' holds
( ( for s being Element of RAT+ st s <=' r holds
s in B' ) & ex s being Element of RAT+ st
( s in B' & r < s ) ) ) ) ;
assume not x c= y ; :: according to XBOOLE_0:def 9 :: thesis: y c= x
then consider s being set such that
A3: s in x and
A4: not s in y by TARSKI:def 3;
reconsider s = s as Element of RAT+ by A1, A3;
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in y or e in x )
assume A5: e in y ; :: thesis: e in x
then reconsider r = e as Element of RAT+ by A2;
r <=' s by A2, A4, A5;
hence e in x by A1, A3; :: thesis: verum