set D = the non empty (F2) (F1) (F3) (F4) Dependency-set of X;
reconsider D = the non empty (F2) (F1) (F3) (F4) Dependency-set of X as Full-family of X by Def14;
take D ; :: thesis: D is finite
thus D is finite ; :: thesis: verum