for v being LTL-formula
for w being Element of Inf_seq AtomicFamily
for U being Choice_Function of (BOOL (Subformulae v)) holds choice_succ_func (w,v,U) is_succ_homomorphism v,w