:: deftheorem defines -firstChar FOMODEL0:def 11 :
for D being non empty set holds D -firstChar = MultPlace (D -pr1);