for v being LTL-formula ex f being Choice_Function of (BOOL (Subformulae v)) st f is Function of (BOOL (Subformulae v)),(Subformulae v)