let A be non empty Subset of RAT+ ; :: thesis: ( A in RAT+ implies ex s being Element of RAT+ st
( s in A & ( for r being Element of RAT+ st r in A holds
r <=' s ) ) )
assume A1: A in RAT+ ; :: thesis: ex s being Element of RAT+ st
( s in A & ( for r being Element of RAT+ st r in A holds
r <=' s ) )

now

given i, j being Element of omega such that A2: ( A = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 ) ; :: thesis: contradiction
A3: {i} in A by A2, TARSKI:def 2;

now

assume {i} in omega ; :: thesis: contradiction
then {i} is Ordinal ;
then {} in {i} by ORDINAL3:10;
then {} = i by TARSKI:def 1;
hence contradiction by A2, Th7; :: thesis: verum

end;

then consider i1, j1 being Element of omega such that
A4: ( {i} = [i1,j1] & i1,j1 are_relative_prime & j1 <> {} & j1 <> 1 ) by A3, Th35;
( {i1} in {i} & {i1,j1} in {i} ) by A4, TARSKI:def 2;
then ( i = {i1} & i = {i1,j1} ) by TARSKI:def 1;
then j1 in {i1} by TARSKI:def 2;
then ( j1 = i1 & j1 = j1 *^ 1 ) by ORDINAL2:56, TARSKI:def 1;
hence contradiction by A4, Def2; :: thesis: verum

end;

then reconsider B = A as Element of omega by A1, Th35;
A5: {} in B by ORDINAL3:10;

now

assume B is limit_ordinal ; :: thesis: contradiction
then omega c= B by A5, ORDINAL1:def 12;
hence contradiction by ORDINAL1:7; :: thesis: verum

end;

then consider C being Ordinal such that
A6: B = succ C by ORDINAL1:42;
C in B by A6, ORDINAL1:10;
then reconsider C = C as ordinal Element of RAT+ ;
take C ; :: thesis: ( C in A & ( for r being Element of RAT+ st r in A holds
r <=' C ) )
thus C in A by A6, ORDINAL1:10; :: thesis: for r being Element of RAT+ st r in A holds
r <=' C
let r be Element of RAT+ ; :: thesis: ( r in A implies r <=' C )
assume A7: r in A ; :: thesis: r <=' C
then r in B ;
then reconsider r = r as ordinal Element of RAT+ ;
C -^ r in omega by ORDINAL1:def 13;
then reconsider x = C -^ r as ordinal Element of RAT+ by Lm5;
r c= C by A6, A7, ORDINAL1:34;
then C = r +^ x by ORDINAL3:def 6
.= r + x by Th64 ;
hence r <=' C by Def13; :: thesis: verum