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

take B ; :: thesis: ( not B is empty & B is reflexive )

thus ( not B is empty & B is reflexive ) ; :: thesis: verum