let X be non empty natural-membered set ; :: thesis: ( ( for a being Nat st a in X holds
ex b being Nat st
( b > a & b in X ) ) implies X is infinite )
assume A1: for a being Nat st a in X holds
ex b being Nat st
( b > a & b in X ) ; :: thesis: X is infinite
assume X is finite ; :: thesis: contradiction
then reconsider X = X as non empty finite ext-real-membered set ;
max X in X by XXREAL_2:def 8;
then ex b being Nat st
( b > max X & b in X ) by A1;
hence contradiction by XXREAL_2:def 8; :: thesis: verum