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 (QC-symbols A) by Lm2, QC_LANG1:3, XBOOLE_1:109; :: thesis: verum