for P being PNPair
for Q being Element of untn P holds {} LTLB_WFF |- (P ^) => ('X' (Q ^))