let B, C be Element of LTLB_WFF ; :: thesis: for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,((B 'U' C) => ('X' ('F' C)))] = 1
let n be Element of NAT ; :: thesis: for M being LTLModel holds (SAT M) . [n,((B 'U' C) => ('X' ('F' C)))] = 1
let M be LTLModel; :: thesis: (SAT M) . [n,((B 'U' C) => ('X' ('F' C)))] = 1
set sm = SAT M;

A1: now :: thesis: ( (SAT M) . [n,(B 'U' C)] = 1 implies not (SAT M) . [n,('X' ('F' C))] = 0 )

assume that
A2: (SAT M) . [n,(B 'U' C)] = 1 and
A3: (SAT M) . [n,('X' ('F' C))] = 0 ; :: thesis: contradiction
consider i being Element of NAT such that
A4: 0 < i and
A5: (SAT M) . [(n + i),C] = 1 and
for j being Element of NAT st 1 <= j & j < i holds
(SAT M) . [(n + j),B] = 1 by A2, Def11;
i + (- 1) >= 1 + (- 1) by A4, NAT_1:25, XREAL_1:6;
then A6: (n + 1) + (i -' 1) = (n + 1) + (i - 1) by XREAL_0:def 2
.= n + i ;
(SAT M) . [(n + 1),('F' C)] = 0 by A3, Th9;
hence contradiction by A5, A6, Th11; :: thesis: verum

end;

( (SAT M) . [n,(B 'U' C)] = 0 or (SAT M) . [n,(B 'U' C)] = 1 ) by XBOOLEAN:def 3;
then ((SAT M) . [n,(B 'U' C)]) => ((SAT M) . [n,('X' ('F' C))]) = 1 by A1, XBOOLEAN:def 3;
hence (SAT M) . [n,((B 'U' C) => ('X' ('F' C)))] = 1 by Def11; :: thesis: verum