let A be Ordinal; :: thesis: A -^ A = {}
( A +^ {} = A & A c= A ) by ORDINAL2:44;
hence A -^ A = {} by Def6; :: thesis: verum