A: l in NAT by ORDINAL1:def 13;
ObjectKind (IC S) = NAT by Def11;
hence (IC S) .--> l is FinPartState of S by Th59, A; :: thesis: verum