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 (DC3) & the non empty (F2) (F1) (F3) (F4) Dependency-set of X is (F2) & the non empty (F2) (F1) (F3) (F4) Dependency-set of X is (F4) & not the non empty (F2) (F1) (F3) (F4) Dependency-set of X is empty )
thus ( the non empty (F2) (F1) (F3) (F4) Dependency-set of X is (DC3) & the non empty (F2) (F1) (F3) (F4) Dependency-set of X is (F2) & the non empty (F2) (F1) (F3) (F4) Dependency-set of X is (F4) & not the non empty (F2) (F1) (F3) (F4) Dependency-set of X is empty ) ; :: thesis: verum