let n be Nat; :: thesis: for V being LTLModel
for Kai being Function of atomic_LTL, the BasicAssign of V holds EvalSet (V,Kai,n) in EvalFamily (V,Kai)
let V be LTLModel; :: thesis: for Kai being Function of atomic_LTL, the BasicAssign of V holds EvalSet (V,Kai,n) in EvalFamily (V,Kai)
let Kai be Function of atomic_LTL, the BasicAssign of V; :: thesis: EvalSet (V,Kai,n) in EvalFamily (V,Kai)
set p1 = EvalSet (V,Kai,n);
EvalSet (V,Kai,n) 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,n) or x in Funcs (LTL_WFF, the carrier of V) )
assume x in EvalSet (V,Kai,n) ; :: 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 n,Kai ) ;
hence x in Funcs (LTL_WFF, the carrier of V) by FUNCT_2:8; :: thesis: verum

end;

hence EvalSet (V,Kai,n) in EvalFamily (V,Kai) by Def34; :: thesis: verum