defpred S₁[ set ] means ( $1 in bool (Funcs LTL_WFF ,the Assignations 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 S₁[x] ) ) & ( for x being set holds
( x in X2 iff S₁[x] ) ) holds
X1 = X2 from XBOOLE_0:sch 3();
hence for b₁, b₂ being non empty set st ( for p being set holds
( p in b₁ iff ( p in bool (Funcs LTL_WFF ,the Assignations of V) & ex n being Nat st p = EvalSet V,Kai,n ) ) ) & ( for p being set holds
( p in b₂ iff ( p in bool (Funcs LTL_WFF ,the Assignations of V) & ex n being Nat st p = EvalSet V,Kai,n ) ) ) holds
b₁ = b₂ ; :: thesis: verum