let A be Subset of REAL ; :: thesis: ( 0 in A & ( for x being real number st x in A holds
x + 1 in A ) implies NAT c= A )
assume that
A1:
0 in A
and
A2:
for x being real number st x in A holds
x + 1 in A
; :: thesis: NAT c= A
reconsider B = A /\ REAL+ as Subset of REAL+ by XBOOLE_1:17;
A3:
0 in B
by A1, ARYTM_2:21, XBOOLE_0:def 4;
A4:
B c= A
by XBOOLE_1:17;
for x', y' being Element of REAL+ st x' in B & y' = 1 holds
x' + y' in B
proof
let x',
y' be
Element of
REAL+ ;
:: thesis: ( x' in B & y' = 1 implies x' + y' in B )
assume that A5:
x' in B
and A6:
y' = 1
;
:: thesis: x' + y' in B
x' in REAL+
;
then reconsider x =
x' as
Element of
REAL by ARYTM_0:1;
reconsider xx =
x as
real number by XREAL_0:def 1;
consider x'',
y'' being
Element of
REAL+ such that A7:
x = x''
and A8:
1
= y''
and A9:
+ x,1
= x'' + y''
by ARYTM_0:def 2, ARYTM_2:21;
xx + 1
in A
by A2, A4, A5;
then
+ x,1
in A
by Lm3;
hence
x' + y' in B
by A6, A7, A8, A9, XBOOLE_0:def 4;
:: thesis: verum
end;
then
NAT c= B
by A3, ARYTM_2:18;
hence
NAT c= A
by A4, XBOOLE_1:1; :: thesis: verum