let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for l1, l2 being Element of NAT st SUCC (l1,S) = NAT holds
l1 <= l2,S
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: for l1, l2 being Element of NAT st SUCC (l1,S) = NAT holds
l1 <= l2,S
let l1, l2 be Element of NAT ; :: thesis: ( SUCC (l1,S) = NAT implies l1 <= l2,S )
assume A1: SUCC (l1,S) = NAT ; :: thesis: l1 <= l2,S
defpred S₁[ set , set ] means ( ( $1 = 1 implies $2 = l1 ) & ( $1 = 2 implies $2 = l2 ) );
A2: for n being Nat st n in Seg 2 holds
ex d being Element of NAT st S₁[n,d]

proof

let n be Nat; :: thesis: ( n in Seg 2 implies ex d being Element of NAT st S₁[n,d] )
assume A3: n in Seg 2 ; :: thesis: ex d being Element of NAT st S₁[n,d]

per cases ( n = 1 or n = 2 ) by A3, FINSEQ_1:2, TARSKI:def 2;

suppose A4: n = 1 ; :: thesis: ex d being Element of NAT st S₁[n,d]

reconsider l1 = l1 as Element of NAT ;
take l1 ; :: thesis: S₁[n,l1]
thus S₁[n,l1] by A4; :: thesis: verum

end;

suppose A5: n = 2 ; :: thesis: ex d being Element of NAT st S₁[n,d]

reconsider l2 = l2 as Element of NAT ;
take l2 ; :: thesis: S₁[n,l2]
thus S₁[n,l2] by A5; :: thesis: verum

end;

end;

end;

consider f being FinSequence of NAT such that
A6: len f = 2 and
A7: for n being Nat st n in Seg 2 holds
S₁[n,f /. n] from FINSEQ_4:sch 1(A2);
A8: 1 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
then A9: f /. 1 = l1 by A7;
reconsider f = f as non empty FinSequence of NAT by A6;
take f ; :: according to AMI_WSTD:def 1 :: thesis: ( f /. 1 = l1 & f /. (len f) = l2 & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) )
2 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
hence ( f /. 1 = l1 & f /. (len f) = l2 ) by A6, A7, A8; :: thesis: for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S)
let n be Element of NAT ; :: thesis: ( 1 <= n & n < len f implies f /. (n + 1) in SUCC ((f /. n),S) )
assume A10: 1 <= n ; :: thesis: ( not n < len f or f /. (n + 1) in SUCC ((f /. n),S) )
assume n < len f ; :: thesis: f /. (n + 1) in SUCC ((f /. n),S)
then n < 1 + 1 by A6;
then n <= 1 by NAT_1:13;
then n = 1 by A10, XXREAL_0:1;
hence f /. (n + 1) in SUCC ((f /. n),S) by A1, A9; :: thesis: verum