take Dependencies X ; :: thesis: ( Dependencies X is (F1) & Dependencies X is (F2) & Dependencies X is (F3) & Dependencies X is (F4) & Dependencies X is (C1) )
thus ( Dependencies X is (F1) & Dependencies X is (F2) & Dependencies X is (F3) & Dependencies X is (F4) & Dependencies X is (C1) ) by Th21; :: thesis: verum