consider C being non empty with_units AltCatStr ;
take C ; :: thesis: ( not C is empty & C is reflexive )
thus ( not C is empty & C is reflexive ) ; :: thesis: verum