set C = the non empty with_units AltCatStr ;
take the non empty with_units AltCatStr ; :: thesis: ( not the non empty with_units AltCatStr is empty & the non empty with_units AltCatStr is reflexive )
thus ( not the non empty with_units AltCatStr is empty & the non empty with_units AltCatStr is reflexive ) ; :: thesis: verum