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)
set Y = Subformulae v;
set X = BOOL (Subformulae v);
for x being set st x in BOOL (Subformulae v) holds
x <> {} by ORDERS_1:1;
then consider Choice being Function such that
A1: dom Choice = BOOL (Subformulae v) and
A2: for x being set st x in BOOL (Subformulae v) holds
Choice . x in x by FUNCT_1:111;
A3: for x being set st x in BOOL (Subformulae v) holds
Choice . x in Subformulae v

proof

let x be set ; :: thesis: ( x in BOOL (Subformulae v) implies Choice . x in Subformulae v )
assume A4: x in BOOL (Subformulae v) ; :: thesis: Choice . x in Subformulae v
not x is empty by A4, ORDERS_1:1;
then A5: x is Subset of (Subformulae v) by A4, ORDERS_1:2;
Choice . x in x by A2, A4;
hence Choice . x in Subformulae v by A5; :: thesis: verum

end;

then A6: Choice is Function of (BOOL (Subformulae v)),(Subformulae v) by A1, FUNCT_2:3;
( not {} in BOOL (Subformulae v) & union (BOOL (Subformulae v)) = Subformulae v ) by Th55, ORDERS_1:1;
then reconsider Choice = Choice as Choice_Function of BOOL (Subformulae v) by A2, A6, ORDERS_1:def 1;
take Choice ; :: thesis: Choice is Function of (BOOL (Subformulae v)),(Subformulae v)
thus Choice is Function of (BOOL (Subformulae v)),(Subformulae v) by A1, A3, FUNCT_2:3; :: thesis: verum