consider X being Subset of ExtNAT such that
A1: for N being set holds
( N in X iff ( N in ExtNAT & P₁[N] ) ) from SUBSET_1:sch 1();
reconsider X = X as ext-natural-membered set ;
take X ; :: thesis: for N being ExtNat holds
( N in X iff P₁[N] )
let N be ExtNat; :: thesis: ( N in X iff P₁[N] )
thus ( N in X implies P₁[N] ) by A1; :: thesis: ( P₁[N] implies N in X )
assume A2: P₁[N] ; :: thesis: N in X
N in ExtNAT by Def1;
hence N in X by A1, A2; :: thesis: verum