let A be Ordinal; :: thesis: A -^ A = {}
A +^ {} = A by ORDINAL2:27;
hence A -^ A = {} by Def6; :: thesis: verum