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

consider X being set such that

A1: for x being object holds

( x in X iff ( x in LTLB_WFF & S

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