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