theorem Th18: :: LTLAXIO4:18

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