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

now :: thesis: not the LTLnew of N = {} v

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

end;

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