defpred S₁[ set ] means ex n being Nat st $1 = EvalSet (V,Kai,n);
set X = bool (Funcs (LTL_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 (LTL_WFF, the carrier of V)) & S₁[p] ) ) from XFAMILY:sch 1();
not IT is empty

proof

set p = EvalSet (V,Kai,0);
EvalSet (V,Kai,0) c= Funcs (LTL_WFF, the carrier of V)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in EvalSet (V,Kai,0) or x in Funcs (LTL_WFF, the carrier of V) )
assume x in EvalSet (V,Kai,0) ; :: thesis: x in Funcs (LTL_WFF, the carrier of V)
then ex h being Function of LTL_WFF, the carrier of V st
( x = h & h is-PreEvaluation-for 0 ,Kai ) ;
hence x in Funcs (LTL_WFF, the carrier of V) by FUNCT_2:8; :: thesis: verum

end;

hence not IT is empty by A1; :: thesis: verum

end;

then reconsider IT = IT as non empty set ;
take IT ; :: thesis: for p being set holds
( p in IT iff ( p in bool (Funcs (LTL_WFF, the carrier of V)) & ex n being Nat st p = EvalSet (V,Kai,n) ) )
thus for p being set holds
( p in IT iff ( p in bool (Funcs (LTL_WFF, the carrier of V)) & ex n being Nat st p = EvalSet (V,Kai,n) ) ) by A1; :: thesis: verum