{ (IC (Following (ProgramPart ss),ss)) where ss is Element of product the Object-Kind of S : ( IC ss = l & (ProgramPart ss) /. l = i ) } c= NAT

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (IC (Following (ProgramPart ss),ss)) where ss is Element of product the Object-Kind of S : ( IC ss = l & (ProgramPart ss) /. l = i ) } or e in NAT )
assume e in { (IC (Following (ProgramPart ss),ss)) where ss is Element of product the Object-Kind of S : ( IC ss = l & (ProgramPart ss) /. l = i ) } ; :: thesis: e in NAT
then ex ss being Element of product the Object-Kind of S st
( e = IC (Following (ProgramPart ss),ss) & IC ss = l & (ProgramPart ss) /. l = i ) ;
hence e in NAT ; :: thesis: verum

end;

hence { (IC (Following (ProgramPart ss),ss)) where ss is Element of product the Object-Kind of S : ( IC ss = l & (ProgramPart ss) /. l = i ) } is Subset of NAT ; :: thesis: verum