let v be LTL-formula; :: thesis: for N being strict LTLnode of v st len N > 0 holds
the LTLnew of N <> {} v
let N be strict LTLnode of v; :: thesis: ( len N > 0 implies the LTLnew of N <> {} v )
assume A1: len N > 0 ; :: thesis: the LTLnew of N <> {} v

now

assume the LTLnew of N = {} v ; :: thesis: contradiction
then len the LTLnew of N = 0 by Th13;
hence contradiction by A1, INT_1:25; :: thesis: verum

end;

hence the LTLnew of N <> {} v ; :: thesis: verum