let A, B be Element of LTLB_WFF ; :: thesis: for P being consistent complete PNPair
for T being pnptree of P st A 'U' B in rng (P `1) & ( for Q being Element of rngr T holds not B in rng (Q `1) ) holds
for Q being Element of rngr T holds
( B in rng (Q `2) & A 'U' B in rng (Q `1) )
set aub = A 'U' B;
let P be consistent complete PNPair; :: thesis: for T being pnptree of P st A 'U' B in rng (P `1) & ( for Q being Element of rngr T holds not B in rng (Q `1) ) holds
for Q being Element of rngr T holds
( B in rng (Q `2) & A 'U' B in rng (Q `1) )
let T be pnptree of P; :: thesis: ( A 'U' B in rng (P `1) & ( for Q being Element of rngr T holds not B in rng (Q `1) ) implies for Q being Element of rngr T holds
( B in rng (Q `2) & A 'U' B in rng (Q `1) ) )
assume that
A1: A 'U' B in rng (P `1) and
A2: for Q being Element of rngr T holds not B in rng (Q `1) ; :: thesis: for Q being Element of rngr T holds
( B in rng (Q `2) & A 'U' B in rng (Q `1) )
defpred S₁[ set ] means for t being Element of dom T st t = $1 & t <> 0 holds
( B in rng ((T . t) `2) & A 'U' B in rng ((T . t) `1) );

A3: now :: thesis: for t being Element of dom T
for n being Nat st S₁[t] & t ^ <*n*> in dom T holds
S₁[t ^ <*n*>]

let t be Element of dom T; :: thesis: for n being Nat st S₁[t] & t ^ <*n*> in dom T holds
S₁[t ^ <*n*>]
let n be Nat; :: thesis: ( S₁[t] & t ^ <*n*> in dom T implies S₁[t ^ <*n*>] )
assume that
A4: S₁[t] and
t ^ <*n*> in dom T ; :: thesis: S₁[t ^ <*n*>]
thus S₁[t ^ <*n*>] :: thesis: verum

proof

let u be Element of dom T; :: thesis: ( u = t ^ <*n*> & u <> 0 implies ( B in rng ((T . u) `2) & A 'U' B in rng ((T . u) `1) ) )
assume that
A5: u = t ^ <*n*> and
u <> 0 ; :: thesis: ( B in rng ((T . u) `2) & A 'U' B in rng ((T . u) `1) )
A6: T . u in rngr T by A5;

per cases ( t = 0 or not t = 0 ) ;

suppose t = 0 ; :: thesis: ( B in rng ((T . u) `2) & A 'U' B in rng ((T . u) `1) )

then T . t = P by Def11;
then reconsider Tu = T . u as Element of compn P by Th26, A5;
( untn (A,B) in rng (Tu `1) & rng (Tu `1) c= rng Tu ) by Th22, A1, XBOOLE_1:7;
then A7: B in rng Tu by Th8;
not B in rng (Tu `1) by A2, A6;
hence ( B in rng ((T . u) `2) & A 'U' B in rng ((T . u) `1) ) by Th25, A1, A7, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A8: not t = 0 ; :: thesis: ( B in rng ((T . u) `2) & A 'U' B in rng ((T . u) `1) )

reconsider Tu = T . u as Element of compn (T . t) by Th26, A5;
( rng (Tu `1) c= rng Tu & untn (A,B) in rng (Tu `1) ) by XBOOLE_1:7, A8, A4, Th22;
then A9: B in rng Tu by Th8;
A10: A 'U' B in rng ((T . t) `1) by A8, A4;
not B in rng (Tu `1) by A2, A6;
hence ( B in rng ((T . u) `2) & A 'U' B in rng ((T . u) `1) ) by A10, A9, Th25, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

end;

let Q be Element of rngr T; :: thesis: ( B in rng (Q `2) & A 'U' B in rng (Q `1) )
Q in rngr T ;
then A11: ex t being Element of dom T st
( Q = T . t & t <> 0 ) ;
A12: S₁[ {} ] ;
for t being Element of dom T holds S₁[t] from TREES_2:sch 1(A12, A3);
hence ( B in rng (Q `2) & A 'U' B in rng (Q `1) ) by A11; :: thesis: verum