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) holds
ex R being Element of rngr T st B in rng (R `1)
let P be consistent complete PNPair; :: thesis: for T being pnptree of P st A 'U' B in rng (P `1) holds
ex R being Element of rngr T st B in rng (R `1)
let T be pnptree of P; :: thesis: ( A 'U' B in rng (P `1) implies ex R being Element of rngr T st B in rng (R `1) )
set nb = 'not' B;
set gnb = 'G' ('not' B);
set xgnb = 'X' ('G' ('not' B));
set aub = A 'U' B;
set f = the Enumeration of (rngr T) ^ ;
set xaf = 'X' H₁( the Enumeration of (rngr T) ^ );
A1: rng the Enumeration of (rngr T) ^ = (rngr T) ^ by RLAFFIN3:def 1;
{} in dom T by TREES_1:22;
then T . {} in rng T by FUNCT_1:3;
then A2: P in rng T by Def11;
reconsider f = the Enumeration of (rngr T) ^ as FinSequence of LTLB_WFF ;
assume A3: A 'U' B in rng (P `1) ; :: thesis: ex R being Element of rngr T st B in rng (R `1)
assume A4: for R being Element of rngr T holds not B in rng (R `1) ; :: thesis: contradiction

now :: thesis: for i being Nat st i in dom f holds
{} LTLB_WFF |- (f /. i) => ('not' B)

let i be Nat; :: thesis: ( i in dom f implies {} LTLB_WFF |- (f /. i) => ('not' B) )
assume i in dom f ; :: thesis: {} LTLB_WFF |- (f /. i) => ('not' B)
then f /. i in (rngr T) ^ by PARTFUN2:2, A1;
then consider R being PNPair such that
A5: f /. i = R ^ and
A6: R in rngr T ;
B in rng (R `2) by Th31, A3, A4, A6;
hence {} LTLB_WFF |- (f /. i) => ('not' B) by LTLAXIO3:29, A5; :: thesis: verum

end;

then A7: {} LTLB_WFF |- H₁(f) => ('not' B) by LTLAXIO2:57;
('X' (H₁(f) => ('G' ('not' B)))) => (('X' H₁( the Enumeration of (rngr T) ^ )) => ('X' ('G' ('not' B)))) in LTL_axioms by LTLAXIO1:def 17;
then A8: {} LTLB_WFF |- ('X' (H₁(f) => ('G' ('not' B)))) => (('X' H₁( the Enumeration of (rngr T) ^ )) => ('X' ('G' ('not' B)))) by LTLAXIO1:42;
{} LTLB_WFF |- H₁(f) => ('X' H₁( the Enumeration of (rngr T) ^ )) by Th29, A1;
then {} LTLB_WFF |- 'X' (H₁(f) => ('G' ('not' B))) by LTLAXIO1:45, A7, LTLAXIO1:44;
then A9: {} LTLB_WFF |- ('X' H₁( the Enumeration of (rngr T) ^ )) => ('X' ('G' ('not' B))) by A8, LTLAXIO1:43;
consider R being object such that
A10: R in untn P by XBOOLE_0:def 1;
reconsider R = R as Element of untn P by A10;
set xr = 'X' (R ^);
set g = the Enumeration of (comp R) ^ ;
reconsider g = the Enumeration of (comp R) ^ as FinSequence of LTLB_WFF ;
A11: rng g = (comp R) ^ by RLAFFIN3:def 1;
(rngr T) ^ = ((comp R) \/ (rngr T)) ^ by Th28, XBOOLE_1:12, A2
.= ((comp R) ^) \/ ((rngr T) ^) by Th10 ;
then H₁(g) => H₁(f) is ctaut by XBOOLE_1:7, A11, A1, LTLAXIO2:30;
then H₁(g) => H₁(f) in LTL_axioms by LTLAXIO1:def 17;
then A12: {} LTLB_WFF |- H₁(g) => H₁(f) by LTLAXIO1:42;
A13: {} LTLB_WFF |- (P ^) => ('X' (R ^)) by Th18;
('X' ((R ^) => H₁(f))) => (('X' (R ^)) => ('X' H₁( the Enumeration of (rngr T) ^ ))) in LTL_axioms by LTLAXIO1:def 17;
then A14: {} LTLB_WFF |- ('X' ((R ^) => H₁(f))) => (('X' (R ^)) => ('X' H₁( the Enumeration of (rngr T) ^ ))) by LTLAXIO1:42;
{} LTLB_WFF |- (R ^) => H₁(g) by A11, Th17;
then {} LTLB_WFF |- 'X' ((R ^) => H₁(f)) by A12, LTLAXIO1:47, LTLAXIO1:44;
then {} LTLB_WFF |- ('X' (R ^)) => ('X' H₁( the Enumeration of (rngr T) ^ )) by LTLAXIO1:43, A14;
then {} LTLB_WFF |- (P ^) => ('X' H₁( the Enumeration of (rngr T) ^ )) by LTLAXIO1:47, A13;
then A15: {} LTLB_WFF |- (P ^) => ('X' ('G' ('not' B))) by LTLAXIO1:47, A9;
A16: {} LTLB_WFF |- (P ^) => (A 'U' B) by LTLAXIO3:28, A3;
(A 'U' B) => ('X' ('F' B)) in LTL_axioms by LTLAXIO1:def 17;
then A17: {} LTLB_WFF |- (A 'U' B) => ('X' ('F' B)) by LTLAXIO1:42;
('X' ('F' B)) => ('not' ('X' ('G' ('not' B)))) in LTL_axioms by LTLAXIO1:def 17;
then {} LTLB_WFF |- ('X' ('F' B)) => ('not' ('X' ('G' ('not' B)))) by LTLAXIO1:42;
then {} LTLB_WFF |- (A 'U' B) => ('not' ('X' ('G' ('not' B)))) by A17, LTLAXIO1:47;
then {} LTLB_WFF |- (P ^) => ('not' ('X' ('G' ('not' B)))) by LTLAXIO1:47, A16;
then {} LTLB_WFF |- (P ^) => (('X' ('G' ('not' B))) '&&' ('not' ('X' ('G' ('not' B))))) by A15, LTLAXIO2:52;
then {} LTLB_WFF |- 'not' (P ^) by LTLAXIO2:55;
hence contradiction by LTLAXIO3:def 10; :: thesis: verum