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