let A, B be Ordinal; :: thesis: ( A +^ B = {} implies ( A = {} & B = {} ) )
assume A +^ B = {} ; :: thesis: ( A = {} & B = {} )
then ( A c= {} & B c= {} ) by Th27;
hence ( A = {} & B = {} ) by XBOOLE_1:3; :: thesis: verum