<^o,o^> <> {} by ALTCAT_1:19;
hence A * B is mono by Th9; :: thesis: verum