set IR = { 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 ) ) } ;
let x, y be set ; :: according to ORDINAL1:def 8 :: thesis: ( not x 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 ) ) } or not 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 ) ) } or x,y are_c=-comparable )
assume x 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: ( not 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 ) ) } or x,y are_c=-comparable )
then A1: ex A9 being Subset of RAT+ st
( x = A9 & ( for r being Element of RAT+ st r in A9 holds
( ( for s being Element of RAT+ st s <=' r holds
s in A9 ) & ex s being Element of RAT+ st
( s in A9 & r < s ) ) ) ) ;
assume 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: x,y are_c=-comparable
then A2: ex B9 being Subset of RAT+ st
( y = B9 & ( for r being Element of RAT+ st r in B9 holds
( ( for s being Element of RAT+ st s <=' r holds
s in B9 ) & ex s being Element of RAT+ st
( s in B9 & r < s ) ) ) ) ;
assume not x c= y ; :: according to XBOOLE_0:def 9 :: thesis: y c= x
then consider s being object such that
A3: s in x and
A4: not s in y ;
reconsider s = s as Element of RAT+ by A1, A3;
let e be object ; :: 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