:: deftheorem defines really-closed AMISTD_1:def 9 :
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for F being preProgram of S holds
( F is really-closed iff for l being Nat st l in dom F holds
NIC ((F /. l),l) c= dom F );