let n be Element of NAT ; :: thesis: for V being CTLModelStr
for Kai being Function of atomic_WFF ,the BasicAssign of V holds EvalSet V,Kai,n in EvalFamily V,Kai
let V be CTLModelStr ; :: 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 Assignations of V

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in EvalSet V,Kai,n or x in Funcs CTL_WFF ,the Assignations of V )
assume x in EvalSet V,Kai,n ; :: thesis: x in Funcs CTL_WFF ,the Assignations of V
then ex h being Function of CTL_WFF ,the Assignations of V st
( x = h & h is-PreEvaluation-for n,Kai ) ;
hence x in Funcs CTL_WFF ,the Assignations of V by FUNCT_2:11; :: thesis: verum

end;

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