let X be non empty ext-natural-membered set ; :: thesis: ex N being ExtNat st N in X
consider x being ExtReal such that
A1: x in X by MEMBERED:8;
reconsider N = x as ext-natural ExtReal by A1;
take N ; :: thesis: N in X
thus N in X by A1; :: thesis: verum