let v be LTL-formula; :: thesis: ex f being Choice_Function of (BOOL (Subformulae v)) st f is Function of (BOOL (Subformulae v)),(Subformulae v)
take f = the Choice_Function of (BOOL (Subformulae v)); :: thesis: f is Function of (BOOL (Subformulae v)),(Subformulae v)
A1: not {} in BOOL (Subformulae v) by ORDERS_1:1;
union (BOOL (Subformulae v)) = Subformulae v by Th55;
hence f is Function of (BOOL (Subformulae v)),(Subformulae v) by ORDERS_1:90, A1; :: thesis: verum