let A be non empty Subset of RAT+; ( 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 for i, j being Element of omega holds
( not A = [i,j] or not i,j are_coprime 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_coprime
and
j <> {}
and A4:
j <> 1
;
contradiction
{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_coprime
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;
verum end;
assume
A in RAT+
; 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;
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
; ( C in A & ( for r being Element of RAT+ st r in A holds
r <=' C ) )
thus
C in A
by A12, ORDINAL1:6; for r being Element of RAT+ st r in A holds
r <=' C
let r be Element of RAT+ ; ( r in A implies r <=' C )
assume A13:
r in A
; 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 Lm6;
r c= C
by A12, A13, ORDINAL1:22;
then C =
r +^ x
by ORDINAL3:def 5
.=
r + x
by Th58
;
hence
r <=' C
; verum