reconsider F = {} as Function-yielding Function ;
F is X -support-yielding ;
hence ex b₁ being Function-yielding Function st b₁ is X -support-yielding ; :: thesis: verum