let n be Nat; 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; 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; 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)
hence
EvalSet (V,Kai,n) in EvalFamily (V,Kai)
by Def34; verum