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