let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {<*2,3,7,42*>,<*2,3,8,24*>} or x in IncreasingSolutionsOfSumOfReciprocals 4 )
assume x in {<*2,3,7,42*>,<*2,3,8,24*>} ; :: thesis: x in IncreasingSolutionsOfSumOfReciprocals 4
then ( x = <*2,3,7,42*> or x = <*2,3,8,24*> ) by TARSKI:def 2;
hence x in IncreasingSolutionsOfSumOfReciprocals 4 by Th119, Th120; :: thesis: verum