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 XBOOLE_0: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 set ; :: 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:11; :: 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