let k be Nat; :: thesis: ( k <> 0 & S₁[k] implies ex l being Nat st
( l < k & S₁[l] ) )
assume that
A5: k <> 0 and
A6: S₁[k] ; :: thesis: ex l being Nat st
( l < k & S₁[l] )
reconsider k1 = k + 1 as non zero Element of NAT ;
k > 0 by A5, NAT_1:3;
then k + 1 > 0 + 1 by XREAL_1:6;
then consider n being non zero Element of NAT such that
A7: n < k1 and
A8: P₁[n] by A2, A6;
consider l being Nat such that
A9: n = l + 1 by NAT_1:6;
take l = l; :: thesis: ( l < k & S₁[l] )
thus l < k by A7, A9, XREAL_1:6; :: thesis: S₁[l]
thus S₁[l] by A8, A9; :: thesis: verum