set D = the non empty (F2) (F1) (F3) (F4) Dependency-set of X;
take the non empty (F2) (F1) (F3) (F4) Dependency-set of X ; :: thesis: the non empty (F2) (F1) (F3) (F4) Dependency-set of X is full_family
thus the non empty (F2) (F1) (F3) (F4) Dependency-set of X is full_family ; :: thesis: verum