:: deftheorem defines EmptyIns AOFA_000:def 16 :
for A being non-empty with_empty-instruction UAStr holds EmptyIns A = (Den ((In (1,(dom the charact of A))),A)) . {};