let A, B, p, q be Element of LTLB_WFF ; :: thesis: ( p in Sub . (A 'U' B) & A 'U' B in Sub . q implies p in Sub . q )
set aub = A 'U' B;
set f = TFALSUM ;
defpred S1[ Element of LTLB_WFF ] means ( A 'U' B in Sub . $1 implies p in Sub . $1 );
A1: for n being Element of NAT holds S1[ prop n]
proof
let n be Element of NAT ; :: thesis: S1[ prop n]
set pr = prop n;
assume A 'U' B in Sub . (prop n) ; :: thesis: p in Sub . (prop n)
then A 'U' B in {(prop n)} by Def6;
then A 'U' B = prop n by TARSKI:def 1;
hence p in Sub . (prop n) by HILBERT2:24; :: thesis: verum
end;
assume A2: p in Sub . (A 'U' B) ; :: thesis: ( not A 'U' B in Sub . q or p in Sub . q )
A3: for r, s being Element of LTLB_WFF st S1[r] & S1[s] holds
( S1[r 'U' s] & S1[r => s] )
proof
let r, s be Element of LTLB_WFF ; :: thesis: ( S1[r] & S1[s] implies ( S1[r 'U' s] & S1[r => s] ) )
assume that
A4: S1[r] and
A5: S1[s] ; :: thesis: ( S1[r 'U' s] & S1[r => s] )
thus S1[r 'U' s] :: thesis: S1[r => s]
proof
set f = r 'U' s;
A6: tau1 . r c= Sub . r by Th25;
A7: Sub . (r 'U' s) = ((tau1 . (untn (r,s))) \/ (Sub . r)) \/ (Sub . s) by Def6;
then A8: Sub . s c= Sub . (r 'U' s) by XBOOLE_1:7;
( Sub . r c= (tau1 . (untn (r,s))) \/ (Sub . r) & (tau1 . (untn (r,s))) \/ (Sub . r) c= Sub . (r 'U' s) ) by XBOOLE_1:7, A7;
then A9: Sub . r c= Sub . (r 'U' s) ;
assume A 'U' B in Sub . (r 'U' s) ; :: thesis: p in Sub . (r 'U' s)
then A10: A 'U' B in ((tau1 . (untn (r,s))) \/ (Sub . r)) \/ (Sub . s) by Def6;
A11: tau1 . s c= Sub . s by Th25;
per cases ( A 'U' B in (tau1 . (untn (r,s))) \/ (Sub . r) or A 'U' B in Sub . s ) by A10, XBOOLE_0:def 3;
suppose A12: A 'U' B in (tau1 . (untn (r,s))) \/ (Sub . r) ; :: thesis: p in Sub . (r 'U' s)
per cases ( A 'U' B in tau1 . (untn (r,s)) or A 'U' B in Sub . r ) by A12, XBOOLE_0:def 3;
suppose A 'U' B in tau1 . (untn (r,s)) ; :: thesis: p in Sub . (r 'U' s)
then A 'U' B in tau1 . (('not' s) '&&' ('not' (r '&&' (r 'U' s)))) by Th9;
then ( A 'U' B in tau1 . ('not' s) or A 'U' B in tau1 . ('not' (r '&&' (r 'U' s))) ) by Th10;
then A13: ( A 'U' B in tau1 . s or A 'U' B in tau1 . (r '&&' (r 'U' s)) ) by Th9;
per cases ( A 'U' B in tau1 . r or A 'U' B in tau1 . s or A 'U' B in tau1 . (r 'U' s) ) by A13, Th10;
suppose A14: ( A 'U' B in tau1 . r or A 'U' B in tau1 . s ) ; :: thesis: p in Sub . (r 'U' s)
per cases ( A 'U' B in tau1 . r or A 'U' B in tau1 . s ) by A14;
suppose A 'U' B in tau1 . r ; :: thesis: p in Sub . (r 'U' s)
hence p in Sub . (r 'U' s) by A6, A4, A9; :: thesis: verum
end;
suppose A 'U' B in tau1 . s ; :: thesis: p in Sub . (r 'U' s)
hence p in Sub . (r 'U' s) by A11, A5, A8; :: thesis: verum
end;
end;
end;
suppose A 'U' B in tau1 . (r 'U' s) ; :: thesis: p in Sub . (r 'U' s)
then A 'U' B in {(r 'U' s)} by Def4;
hence p in Sub . (r 'U' s) by TARSKI:def 1, A2; :: thesis: verum
end;
end;
end;
suppose A 'U' B in Sub . r ; :: thesis: p in Sub . (r 'U' s)
hence p in Sub . (r 'U' s) by A4, A9; :: thesis: verum
end;
end;
end;
suppose A 'U' B in Sub . s ; :: thesis: p in Sub . (r 'U' s)
hence p in Sub . (r 'U' s) by A5, A8; :: thesis: verum
end;
end;
end;
thus S1[r => s] :: thesis: verum
proof
set f = r => s;
A15: Sub . (r => s) = ({(r => s)} \/ (Sub . r)) \/ (Sub . s) by Def6;
then A16: Sub . s c= Sub . (r => s) by XBOOLE_1:7;
( Sub . r c= {(r => s)} \/ (Sub . r) & {(r => s)} \/ (Sub . r) c= Sub . (r => s) ) by XBOOLE_1:7, A15;
then A17: Sub . r c= Sub . (r => s) ;
assume A 'U' B in Sub . (r => s) ; :: thesis: p in Sub . (r => s)
then A18: A 'U' B in ({(r => s)} \/ (Sub . r)) \/ (Sub . s) by Def6;
per cases ( A 'U' B in {(r => s)} \/ (Sub . r) or A 'U' B in Sub . s ) by A18, XBOOLE_0:def 3;
suppose A19: A 'U' B in {(r => s)} \/ (Sub . r) ; :: thesis: p in Sub . (r => s)
per cases ( A 'U' B in {(r => s)} or A 'U' B in Sub . r ) by A19, XBOOLE_0:def 3;
suppose A 'U' B in {(r => s)} ; :: thesis: p in Sub . (r => s)
then A 'U' B = r => s by TARSKI:def 1;
hence p in Sub . (r => s) by HILBERT2:22; :: thesis: verum
end;
suppose A 'U' B in Sub . r ; :: thesis: p in Sub . (r => s)
hence p in Sub . (r => s) by A4, A17; :: thesis: verum
end;
end;
end;
suppose A 'U' B in Sub . s ; :: thesis: p in Sub . (r => s)
hence p in Sub . (r => s) by A5, A16; :: thesis: verum
end;
end;
end;
end;
A20: S1[ TFALSUM ]
proof
assume A 'U' B in Sub . TFALSUM ; :: thesis: p in Sub . TFALSUM
then A 'U' B in {TFALSUM} by Def6;
then A 'U' B = TFALSUM by TARSKI:def 1;
hence p in Sub . TFALSUM by HILBERT2:23; :: thesis: verum
end;
for p being Element of LTLB_WFF holds S1[p] from HILBERT2:sch 2(A20, A1, A3);
 hence ( not A 'U' B in Sub . q or p in Sub . q ) ; :: thesis: verum