:: deftheorem defines IncreasingSolutionsOfSumOfReciprocals NUMBER17:def 14 :
for s being Nat holds IncreasingSolutionsOfSumOfReciprocals s = { f where f is b₁ -element natural-valued increasing positive-yielding FinSequence : f is with_sum_of_reciprocals_equal_1 } ;