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, INT_1:25; :: thesis: verum
end;
hence the LTLnew of N <> {} v ; :: thesis: verum