set X = (Dom_Bound_Vars p) \/ (Sub_Var finSub);
card ((Dom_Bound_Vars p) \/ (Sub_Var finSub)) in card NAT by CARD_3:58;
hence NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub)) is non empty Subset of NAT by CARD_2:4, XBOOLE_1:36; :: thesis: verum