( a is Real & b in NAT ) by ORDINAL1:def 13, XREAL_0:def 1;
hence not a |^ b is empty by CARD_4:51; :: thesis: verum