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