Minor polish in pred_set + theorem about CARD(BIGUNION s)