let s be Nat; :: thesis: IncreasingSolutionsOfSumOfReciprocals s c= SolutionsOfSumOfReciprocals s
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in IncreasingSolutionsOfSumOfReciprocals s or x in SolutionsOfSumOfReciprocals s )
assume x in IncreasingSolutionsOfSumOfReciprocals s ; :: thesis: x in SolutionsOfSumOfReciprocals s
then ex f being s -element natural-valued increasing positive-yielding FinSequence st
( x = f & f is with_sum_of_reciprocals_equal_1 ) ;
hence x in SolutionsOfSumOfReciprocals s ; :: thesis: verum