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