let T be finite-branching Tree; :: thesis: ( not T is finite implies ex B being Branch of T st not B is finite )
assume not T is finite ; :: thesis: not for B being Branch of T holds B is finite
then consider C being Chain of T such that
A1: not C is finite by Th48;
consider B being Branch of T such that
A2: C c= B by TREES_2:28;
not B is finite by A1, A2;
hence not for B being Branch of T holds B is finite ; :: thesis: verum