take Dependencies X ; :: thesis: ( Dependencies X is (F1) & Dependencies X is (F2) & Dependencies X is (F3) & Dependencies X is (F4) & not Dependencies X is empty )
thus ( Dependencies X is (F1) & Dependencies X is (F2) & Dependencies X is (F3) & Dependencies X is (F4) & not Dependencies X is empty ) by Th19; :: thesis: verum