:: deftheorem defines -prefix FOMODEL0:def 3 :
for D being non empty set
for X being set holds
( X is D -prefix iff X is D -concatenation -unambiguous );