set X = { h where h is Function of CTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } ;
consider h being Function of CTL_WFF, the carrier of V such that
A1: h is-PreEvaluation-for n,Kai by Lm27;
h in { h where h is Function of CTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } by A1;
hence { h where h is Function of CTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } is non empty set ; :: thesis: verum