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