theorem :: LTLAXIO2:60

for f being FinSequence of LTLB_WFF holds {} LTLB_WFF |- ((con (nex f)) /. (len (con (nex f)))) => ('X' ((con f) /. (len (con f))))