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