let A be Ordinal; :: thesis: ( A -^ {} = A & {} -^ A = {} )
A1: ( {} c= A & {} +^ A = A ) by ORDINAL2:47, XBOOLE_1:2;
hence A -^ {} = A by Def6; :: thesis: {} -^ A = {}
( not A c= {} or A c= {} ) ;
then ( {} -^ A = {} or A = {} ) by Def6, XBOOLE_1:3;
hence {} -^ A = {} by A1, Def6; :: thesis: verum