a is Real by XREAL_0:def 1;
hence not a |^ b is empty by CARD_4:51; :: thesis: verum