theorem Th20: :: LTLAXIO1:20

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