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 ) ) )

A1: now :: thesis: for i, j being Element of omega holds
( not A = [i,j] or not i,j are_relative_prime or not j <> {} or not j <> 1 )

given i, j being Element of omega such that A2: A = [i,j] and
A3: i,j are_relative_prime and
j <> {} and
A4: j <> 1 ; :: thesis: contradiction

A5: now :: thesis: not {i} in omega

assume {i} in omega ; :: thesis: contradiction
then {} in {i} by ORDINAL3:8;
then {} = i by TARSKI:def 1;
hence contradiction by A3, A4, Th3; :: thesis: verum

end;

{i} in A by A2, TARSKI:def 2;
then consider i1, j1 being Element of omega such that
A6: {i} = [i1,j1] and
A7: i1,j1 are_relative_prime and
j1 <> {} and
A8: j1 <> 1 by A5, Th29;
{i1,j1} in {i} by A6, TARSKI:def 2;
then A9: i = {i1,j1} by TARSKI:def 1;
{i1} in {i} by A6, TARSKI:def 2;
then i = {i1} by TARSKI:def 1;
then j1 in {i1} by A9, TARSKI:def 2;
then A10: j1 = i1 by TARSKI:def 1;
j1 = j1 *^ 1 by ORDINAL2:39;
hence contradiction by A7, A8, A10, Def2; :: thesis: verum

end;

assume 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 ) )
then reconsider B = A as Element of omega by A1, Th29;
A11: {} in B by ORDINAL3:8;

now :: thesis: not B is limit_ordinal

assume B is limit_ordinal ; :: thesis: contradiction
then omega c= B by A11, ORDINAL1:def 11;
hence contradiction by ORDINAL1:5; :: thesis: verum

end;

then consider C being Ordinal such that
A12: B = succ C by ORDINAL1:29;
C in B by A12, ORDINAL1:6;
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 A12, ORDINAL1:6; :: 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 A13: 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 12;
then reconsider x = C -^ r as ordinal Element of RAT+ by Lm5;
r c= C by A12, A13, ORDINAL1:22;
then C = r +^ x by ORDINAL3:def 5
.= r + x by Th58 ;
hence r <=' C by Def13; :: thesis: verum