reconsider B = A as SubCatStr of A by ALTCAT_2:20;
take B ; :: thesis: ( not B is empty & B is reflexive )
thus ( not B is empty & B is reflexive ) ; :: thesis: verum