let n be Element of NAT ; 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; 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; 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)
hence
EvalSet (V,Kai,n) in EvalFamily (V,Kai)
by Def33; verum