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

end;

hence EvalSet V,Kai,n in EvalFamily V,Kai by Def32; :: thesis: verum