let X be ARS ; :: thesis: ( X is SN iff for A being set

for z being Element of X holds

( not z in A or ex x being Element of X st

( x in A & ( for y being Element of X holds

( not y in A or not x ==> y ) ) ) ) )

thus ( X is SN implies for A being set

for z being Element of X holds

( not z in A or ex x being Element of X st

( x in A & ( for y being Element of X holds

( not y in A or not x ==> y ) ) ) ) ) :: thesis: ( ( for A being set

for z being Element of X holds

( not z in A or ex x being Element of X st

( x in A & ( for y being Element of X holds

( not y in A or not x ==> y ) ) ) ) ) implies X is SN )

for z being Element of X holds

( not z in A or ex x being Element of X st

( x in A & ( for y being Element of X holds

( not y in A or not x ==> y ) ) ) ) ; :: thesis: X is SN

given f being Function of NAT, the carrier of X such that 01: for i being Nat holds f . i ==> f . (i + 1) ; :: according to ABSRED_0:def 15 :: thesis: contradiction

f . 0 ==> f . (0 + 1) by 01;

then 04: ( not X is empty & 0 in NAT ) by ORDINAL1:def 12;

then 02: f . 0 in rng f by FUNCT_2:4;

for z being Element of X holds

( not z in A or ex x being Element of X st

( x in A & ( for y being Element of X holds

( not y in A or not x ==> y ) ) ) ) )

thus ( X is SN implies for A being set

for z being Element of X holds

( not z in A or ex x being Element of X st

( x in A & ( for y being Element of X holds

( not y in A or not x ==> y ) ) ) ) ) :: thesis: ( ( for A being set

for z being Element of X holds

( not z in A or ex x being Element of X st

( x in A & ( for y being Element of X holds

( not y in A or not x ==> y ) ) ) ) ) implies X is SN )

proof

assume 00:
for A being set
assume 00:
for f being Function of NAT, the carrier of X holds

not for i being Nat holds f . i ==> f . (i + 1) ; :: according to ABSRED_0:def 15 :: thesis: for A being set

for z being Element of X holds

( not z in A or ex x being Element of X st

( x in A & ( for y being Element of X holds

( not y in A or not x ==> y ) ) ) )

given A being set , z being Element of X such that 01: ( z in A & ( for x being Element of X st x in A holds

ex y being Element of X st

( y in A & x ==> y ) ) ) ; :: thesis: contradiction

ex y being Element of X st

( y in A & z ==> y ) by 01;

then reconsider X0 = X as non empty ARS ;

reconsider z0 = z as Element of X0 ;

defpred S_{1}[ Nat, Element of X0, Element of X0] means ( $2 in A implies ( $3 in A & $2 ==> $3 ) );

02: for i being Nat

for x being Element of X0 ex y being Element of X0 st S_{1}[i,x,y]
by 01;

consider f being Function of NAT, the carrier of X0 such that

03: f . 0 = z0 and

04: for i being Nat holds S_{1}[i,f . i,f . (i + 1)]
from RECDEF_1:sch 2(02);

defpred S_{2}[ Nat] means ( f . $1 ==> f . ($1 + 1) & f . $1 in A );

05: S_{2}[ 0 ]
by 01, 03, 04;

_{2}[i]
from NAT_1:sch 2(05, 06);

hence contradiction by 00; :: thesis: verum

end;not for i being Nat holds f . i ==> f . (i + 1) ; :: according to ABSRED_0:def 15 :: thesis: for A being set

for z being Element of X holds

( not z in A or ex x being Element of X st

( x in A & ( for y being Element of X holds

( not y in A or not x ==> y ) ) ) )

given A being set , z being Element of X such that 01: ( z in A & ( for x being Element of X st x in A holds

ex y being Element of X st

( y in A & x ==> y ) ) ) ; :: thesis: contradiction

ex y being Element of X st

( y in A & z ==> y ) by 01;

then reconsider X0 = X as non empty ARS ;

reconsider z0 = z as Element of X0 ;

defpred S

02: for i being Nat

for x being Element of X0 ex y being Element of X0 st S

consider f being Function of NAT, the carrier of X0 such that

03: f . 0 = z0 and

04: for i being Nat holds S

defpred S

05: S

06: now :: thesis: for i being Nat st S_{2}[i] holds

S_{2}[i + 1]

for i being Nat holds SS

let i be Nat; :: thesis: ( S_{2}[i] implies S_{2}[i + 1] )

assume S_{2}[i]
; :: thesis: S_{2}[i + 1]

then f . (i + 1) in A by 04;

hence S_{2}[i + 1]
by 04; :: thesis: verum

end;assume S

then f . (i + 1) in A by 04;

hence S

hence contradiction by 00; :: thesis: verum

for z being Element of X holds

( not z in A or ex x being Element of X st

( x in A & ( for y being Element of X holds

( not y in A or not x ==> y ) ) ) ) ; :: thesis: X is SN

given f being Function of NAT, the carrier of X such that 01: for i being Nat holds f . i ==> f . (i + 1) ; :: according to ABSRED_0:def 15 :: thesis: contradiction

f . 0 ==> f . (0 + 1) by 01;

then 04: ( not X is empty & 0 in NAT ) by ORDINAL1:def 12;

then 02: f . 0 in rng f by FUNCT_2:4;

now :: thesis: for x being Element of X st x in rng f holds

ex y being Element of the carrier of X st

( y in rng f & x ==> y )

hence
contradiction
by 00, 02; :: thesis: verumex y being Element of the carrier of X st

( y in rng f & x ==> y )

let x be Element of X; :: thesis: ( x in rng f implies ex y being Element of the carrier of X st

( y in rng f & x ==> y ) )

assume x in rng f ; :: thesis: ex y being Element of the carrier of X st

( y in rng f & x ==> y )

then consider i being object such that

03: ( i in dom f & x = f . i ) by FUNCT_1:def 3;

reconsider i = i as Element of NAT by 03;

take y = f . (i + 1); :: thesis: ( y in rng f & x ==> y )

thus y in rng f by 04, FUNCT_2:4; :: thesis: x ==> y

thus x ==> y by 01, 03; :: thesis: verum

end;( y in rng f & x ==> y ) )

assume x in rng f ; :: thesis: ex y being Element of the carrier of X st

( y in rng f & x ==> y )

then consider i being object such that

03: ( i in dom f & x = f . i ) by FUNCT_1:def 3;

reconsider i = i as Element of NAT by 03;

take y = f . (i + 1); :: thesis: ( y in rng f & x ==> y )

thus y in rng f by 04, FUNCT_2:4; :: thesis: x ==> y

thus x ==> y by 01, 03; :: thesis: verum