reconsider l = l as Element of NAT by ORDINAL1:def 13;
ObjectKind (IC S) = NAT by Def11;
then (IC S) .--> l is PartState of S by Th5;
hence (IC S) .--> l is FinPartState of S ; :: thesis: verum