let A be Subset of REAL+; :: thesis: ( 0 in A & ( for x, y being Element of REAL+ st x in A & y = one holds
x + y in A ) implies omega c= A )
defpred S1[ set ] means $1 in A;
assume that
A1: S1[ 0 ] and
A2: for x, y being Element of REAL+ st x in A & y = one holds
x + y in A ; :: thesis: omega c= A
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in omega or e in A )
assume e in omega ; :: thesis: e in A
then reconsider a = e as natural Ordinal ;
A3: for a being natural Ordinal st S1[a] holds
S1[ succ a]
proof
reconsider rone = one as Element of REAL+ by Th1;
let a be natural Ordinal; :: thesis: ( S1[a] implies S1[ succ a] )
assume A4: a in A ; :: thesis: S1[ succ a]
reconsider i = a as Element of omega by ORDINAL1:def 12;
A5: a in omega by ORDINAL1:def 12;
then a in RAT+ by Lm5;
then reconsider x = a as Element of REAL+ by Th1;
consider x9, y9 being Element of RAT+ such that
A6: ( x = x9 & rone = y9 ) and
A7: x + rone = x9 + y9 by A5, Lm5, Lm47;
x9 + y9 = i +^ 1 by A6, Lm45
.= succ i by ORDINAL2:31 ;
hence S1[ succ a] by A2, A4, A7; :: thesis: verum
end;
S1[a] from ORDINAL2:sch 17(A1, A3);
hence e in A ; :: thesis: verum