theorem Th21: :: LTLAXIO1:21

for B, C being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,((B 'U' C) => ('X' ('F' C)))] = 1