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 )
proof
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 S1[ 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 S1[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 S1[i,f . i,f . (i + 1)] from RECDEF_1:sch 2(02);
 defpred S2[ Nat] means ( f . $1 ==> f . ($1 + 1) & f . $1 in A );
05: S2[ 0 ] by 01, 03, 04;
06: now :: thesis: for i being Nat st S2[i] holds
S2[i + 1]
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume S2[i] ; :: thesis: S2[i + 1]
then f . (i + 1) in A by 04;
hence S2[i + 1] by 04; :: thesis: verum
end;
for i being Nat holds S2[i] from NAT_1:sch 2(05, 06);
 hence contradiction by 00; :: thesis: verum
end;
assume 00: 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: 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 )
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;
hence contradiction by 00, 02; :: thesis: verum