:: deftheorem defines concrete YELLOW18:def 11 :
for C being category holds
( C is concrete iff ( C is para-functional & C is semi-functional & C is set-id-inheriting ) );