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