let n be Element of NAT ; :: thesis: for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds EvalSet (V,Kai,n) in EvalFamily (V,Kai)
let V be CTLModel; :: thesis: for Kai being Function of atomic_WFF, the BasicAssign of V holds EvalSet (V,Kai,n) in EvalFamily (V,Kai)
let Kai be Function of atomic_WFF, 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 (CTL_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 (CTL_WFF, the carrier of V) )
assume x in EvalSet (V,Kai,n) ; :: thesis: x in Funcs (CTL_WFF, the carrier of V)
then ex h being Function of CTL_WFF, the carrier of V st
( x = h & h is-PreEvaluation-for n,Kai ) ;
hence x in Funcs (CTL_WFF, the carrier of V) by FUNCT_2:8; :: thesis: verum

end;

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