defpred S1[ set ] means ( $1 in bool (Funcs (LTL_WFF, the carrier of V)) & ex n being Nat st $1 = EvalSet (V,Kai,n) );
for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2
from XFAMILY:sch 3();
hence
for b1, b2 being non empty set st ( for p being set holds
( p in b1 iff ( p in bool (Funcs (LTL_WFF, the carrier of V)) & ex n being Nat st p = EvalSet (V,Kai,n) ) ) ) & ( for p being set holds
( p in b2 iff ( p in bool (Funcs (LTL_WFF, the carrier of V)) & ex n being Nat st p = EvalSet (V,Kai,n) ) ) ) holds
b1 = b2
; verum