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);
A0: not {} in BOOL (Subformulae v) by ORDERS_1:4;
A1: union (BOOL (Subformulae v)) = Subformulae v by ThBOOL01;
for x being set st x in BOOL (Subformulae v) holds
x <> {} by ORDERS_1:4;
then consider Choice being Function such that
A4: ( dom Choice = BOOL (Subformulae v) & ( for x being set st x in BOOL (Subformulae v) holds
Choice . x in x ) ) by WELLORD2:28;
A6: 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 B1: x in BOOL (Subformulae v) ; :: thesis: Choice . x in Subformulae v
not x is empty by B1, ORDERS_1:4;
then B2: x is Subset of (Subformulae v) by B1, ORDERS_1:5;
Choice . x in x by B1, A4;
hence Choice . x in Subformulae v by B2; :: thesis: verum

end;

then Choice is Function of (BOOL (Subformulae v)),(Subformulae v) by A4, FUNCT_2:5;
then reconsider Choice = Choice as Choice_Function of BOOL (Subformulae v) by A0, A1, A4, 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 A6, A4, FUNCT_2:5; :: thesis: verum