consider D being non empty (F2) (F1) (F3) (F4) Dependency-set of X;
take D ; :: thesis: D is full_family
thus D is full_family by Def15; :: thesis: verum