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 consider h being Function of CTL_WFF ,the Assignations of V such that
A1: x = h and
h is-PreEvaluation-for n,Kai ;
thus x in Funcs CTL_WFF ,the Assignations of V by A1, FUNCT_2:11; :: thesis: verum

end;

then EvalSet V,Kai,n in bool (Funcs CTL_WFF ,the Assignations of V) ;
hence EvalSet V,Kai,n in EvalFamily V,Kai by Def31; :: thesis: verum