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