not 0 in {6,7,8} ;
hence for k being Element of NAT holds IncAddr (halt SCM+FSA ),k = halt SCM+FSA by Def3, SCMFSA_2:124; :: thesis: verum