consider D being non empty (F2) (F1) (F3) (F4) Dependency-set of X;
take D ; :: thesis: ( D is (DC3) & D is (F2) & D is (F4) & D is (C1) )
thus ( D is (DC3) & D is (F2) & D is (F4) & D is (C1) ) ; :: thesis: verum