defpred S₁[ object ] means ex n being Element of NAT st $1 = prop n;
consider X being set such that
A1: for x being object holds
( x in X iff ( x in LTLB_WFF & S₁[x] ) ) from XBOOLE_0:sch 1();
X c= LTLB_WFF by A1;
then reconsider X = X as Subset of LTLB_WFF ;
take X ; :: thesis: for x being set holds
( x in X iff ex n being Element of NAT st x = prop n )
thus for x being set holds
( x in X iff ex n being Element of NAT st x = prop n ) by A1; :: thesis: verum