:: deftheorem Def16 defines with_units ALTCAT_1:def 16 :
for C being non empty AltCatStr holds
( C is with_units iff ( the Comp of C is with_left_units & the Comp of C is with_right_units ) );