defpred S1[ set ] means ex n being Element of NAT st $1 = EvalSet (V,Kai,n);
set X = bool (Funcs (CTL_WFF, the carrier of V));
consider IT being set such that
A1:
for p being set holds
( p in IT iff ( p in bool (Funcs (CTL_WFF, the carrier of V)) & S1[p] ) )
from XFAMILY:sch 1();
not IT is empty
then reconsider IT = IT as non empty set ;
take
IT
; for p being set holds
( p in IT iff ( p in bool (Funcs (CTL_WFF, the carrier of V)) & ex n being Element of NAT st p = EvalSet (V,Kai,n) ) )
thus
for p being set holds
( p in IT iff ( p in bool (Funcs (CTL_WFF, the carrier of V)) & ex n being Element of NAT st p = EvalSet (V,Kai,n) ) )
by A1; verum