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