defpred S₁[ Nat] means 0 < $1;
consider X being Subset of NAT such that
A1: for n being Element of NAT holds
( n in X iff S₁[n] ) from SUBSET_1:sch 3();
take X ; :: thesis: for n being Nat holds
( n in X iff 0 < n )
let n be Nat; :: thesis: ( n in X iff 0 < n )
thus ( n in X implies 0 < n ) by A1; :: thesis: ( 0 < n implies n in X )
n in NAT by ORDINAL1:def 12;
hence ( 0 < n implies n in X ) by A1; :: thesis: verum