% Leo-III cross-check.
% Proof (a), part 2a (minimal: only the steps this chain uses) -- the aggregate of possibles A exists and has a member other than
% itself: then a Necessary Existent exists (steps 6, 3, 11).
% Vocabulary.  Nothing is assumed about these symbols.
thf(ex_type, type, ex: $i > $o).                     % (ex @ X): X exists
thf(ess_type, type, ess: $i > $o).                   % (ess @ X): X's existence is from its nature
thf(gives_type, type, gives: $i > $i > $o).          % (gives @ Y @ X): Y gives existence to X
thf(nec_type, type, nec: $i > $o).
thf(poss_type, type, poss: $i > $o).
thf(ta_type, type, through_another: $i > $o).
thf(nec_def, definition, nec = (^[X:$i]: ((ex @ X) & (ess @ X)))).            % necessary in itself
thf(poss_def, definition, poss = (^[X:$i]: ((ex @ X) & ~ (ess @ X)))).        % possible in itself
thf(ta_def, definition, through_another = (^[X:$i]: ?[Y:$i]: (gives @ Y @ X))). % something gives X existence
thf(mem_type, type, mem: $i > $i > $o).              % (mem @ P @ A): P is a member of collection A
thf(agg_type, type, agg: $i > $o).
% agg is "the aggregate of all possibles", defined in PR-009 (AggregateOfPossibles); this chain
% needs only the proved steps below, so the definition is left abstract here.
thf(step3, axiom, ![X:$i]: ((poss @ X) => (through_another @ X))).                       % PR-008 possible_requires_murajjih (MP-008)
thf(step6, axiom, ![A:$i]: (((agg @ A) & (ex @ A) & (?[P:$i]: ((P != A) & (poss @ P)))) => (poss @ A))).  % PR-009 aggregate_is_possible (MP-010)
thf(step11, axiom, ![A:$i, C:$i]: (((agg @ A) & (gives @ C @ A)) => (nec @ C))).        % PR-010 cause_is_necessary (MP-011, MP-012)
thf(a_type, type, a: $i).
thf(case_agg, axiom, (agg @ a) & (ex @ a)).
thf(case_member, axiom, ?[Q:$i]: ((Q != a) & (poss @ Q))).
thf(conclusion, conjecture, ?[N:$i]: (nec @ N)).