defpred S_{1}[ 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_{1}[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

consider X being Subset of NAT such that

A1: for n being Element of NAT holds

( n in X iff S

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