theorem Th19: :: LTLAXIO1:19

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' C) 'or' ('X' (B '&&' (B 'U' C)))))] = 1