let v be neg-inner-most LTL-formula; :: thesis: 'X' (CastLTL ({} v)) = {}

now :: thesis: not 'X' (CastLTL ({} v)) <> {}

assume 'X' (CastLTL ({} v)) <> {} ; :: thesis: contradiction
then consider y being object such that
A1: y in 'X' (CastLTL ({} v)) by XBOOLE_0:def 1;
ex x being LTL-formula st
( y = x & ex u being LTL-formula st
( u in CastLTL ({} v) & x = 'X' u ) ) by A1;
hence contradiction ; :: thesis: verum

end;

hence 'X' (CastLTL ({} v)) = {} ; :: thesis: verum