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

now

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

end;

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