let A, B be Element of LTLB_WFF ; :: thesis: for i being Nat
for P being consistent complete PNPair
for T being pnptree of P
for t being path of T st A 'U' B in rng ((T . (t . i)) `2) holds
for j being Element of NAT holds
( not j > i or B in rng ((T . (t . j)) `2) or ex k being Element of NAT st
( i < k & k < j & A in rng ((T . (t . k)) `2) ) )
let i be Nat; :: thesis: for P being consistent complete PNPair
for T being pnptree of P
for t being path of T st A 'U' B in rng ((T . (t . i)) `2) holds
for j being Element of NAT holds
( not j > i or B in rng ((T . (t . j)) `2) or ex k being Element of NAT st
( i < k & k < j & A in rng ((T . (t . k)) `2) ) )
set aub = A 'U' B;
let P be consistent complete PNPair; :: thesis: for T being pnptree of P
for t being path of T st A 'U' B in rng ((T . (t . i)) `2) holds
for j being Element of NAT holds
( not j > i or B in rng ((T . (t . j)) `2) or ex k being Element of NAT st
( i < k & k < j & A in rng ((T . (t . k)) `2) ) )
let T be pnptree of P; :: thesis: for t being path of T st A 'U' B in rng ((T . (t . i)) `2) holds
for j being Element of NAT holds
( not j > i or B in rng ((T . (t . j)) `2) or ex k being Element of NAT st
( i < k & k < j & A in rng ((T . (t . k)) `2) ) )
let t be path of T; :: thesis: ( A 'U' B in rng ((T . (t . i)) `2) implies for j being Element of NAT holds
( not j > i or B in rng ((T . (t . j)) `2) or ex k being Element of NAT st
( i < k & k < j & A in rng ((T . (t . k)) `2) ) ) )
assume A1: A 'U' B in rng ((T . (t . i)) `2) ; :: thesis: for j being Element of NAT holds
( not j > i or B in rng ((T . (t . j)) `2) or ex k being Element of NAT st
( i < k & k < j & A in rng ((T . (t . k)) `2) ) )
given j being Element of NAT such that A2: j > i and
A3: not B in rng ((T . (t . j)) `2) and
A4: for k being Element of NAT st i < k & k < j holds
not A in rng ((T . (t . k)) `2) ; :: thesis: contradiction
A5: j >= i + 1 by A2, NAT_1:13;

per cases ( j = i + 1 or j > i + 1 ) by A5, XXREAL_0:1;

suppose j = i + 1 ; :: thesis: contradiction

then t . j in succ (t . i) by Def13;
then ex n being Nat st
( t . j = (t . i) ^ <*n*> & (t . i) ^ <*n*> in dom T ) ;
then T . (t . j) in compn (T . (t . i)) by Th26;
hence contradiction by Th24, A1, A3; :: thesis: verum

end;

suppose A6: j > i + 1 ; :: thesis: contradiction

i + 1 >= 1 by NAT_1:11;
then reconsider j1 = j - 1 as Element of NAT by XXREAL_0:2, A6, NAT_1:21;
defpred S₁[ Nat] means ( i < $1 & $1 < j implies A 'U' B in rng ((T . (t . $1)) `2) );
j = j1 + 1 ;
then t . j in succ (t . j1) by Def13;
then ex n being Nat st
( t . j = (t . j1) ^ <*n*> & (t . j1) ^ <*n*> in dom T ) ;
then A7: T . (t . j) in compn (T . (t . j1)) by Th26;

A8: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
set k1 = k + 1;
assume A9: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

assume that
A10: i < k + 1 and
A11: k + 1 < j ; :: thesis: A 'U' B in rng ((T . (t . (k + 1))) `2)
A12: i <= k by NAT_1:13, A10;

per cases ( i < k or i = k ) by A12, XXREAL_0:1;

suppose A13: i < k ; :: thesis: A 'U' B in rng ((T . (t . (k + 1))) `2)

set Pk1 = T . (t . (k + 1));
t . (k + 1) in succ (t . k) by Def13;
then ex n being Nat st
( t . (k + 1) = (t . k) ^ <*n*> & (t . k) ^ <*n*> in dom T ) ;
then T . (t . (k + 1)) in compn (T . (t . k)) by Th26;
then ( A in rng ((T . (t . (k + 1))) `2) or A 'U' B in rng ((T . (t . (k + 1))) `2) ) by Th24, A11, NAT_1:16, XXREAL_0:2, A13, A9;
hence A 'U' B in rng ((T . (t . (k + 1))) `2) by A4, A10, A11; :: thesis: verum

end;

suppose A14: i = k ; :: thesis: A 'U' B in rng ((T . (t . (k + 1))) `2)

set Pk1 = T . (t . (k + 1));
t . (k + 1) in succ (t . i) by A14, Def13;
then ex n being Nat st
( t . (k + 1) = (t . i) ^ <*n*> & (t . i) ^ <*n*> in dom T ) ;
then T . (t . (k + 1)) in compn (T . (t . i)) by Th26;
then ( A in rng ((T . (t . (k + 1))) `2) or A 'U' B in rng ((T . (t . (k + 1))) `2) ) by Th24, A1;
hence A 'U' B in rng ((T . (t . (k + 1))) `2) by A4, A10, A11; :: thesis: verum

end;

end;

end;

end;

A15: ( j + (- 1) < j & j + (- 1) > (i + 1) + (- 1) ) by XREAL_1:30, A6, XREAL_1:8;
A16: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A16, A8);
then A 'U' B in rng ((T . (t . j1)) `2) by A15;
hence contradiction by Th24, A7, A3; :: thesis: verum

end;

end;