let A, p, q be Element of LTLB_WFF ; :: thesis: ( p 'U' q in tau1 . ('not' A) implies p 'U' q in tau1 . A )
set a = p 'U' q;
set na = 'not' A;
set f = TFALSUM ;
A1: p 'U' q <> A => TFALSUM by HILBERT2:22;
assume p 'U' q in tau1 . ('not' A) ; :: thesis: p 'U' q in tau1 . A
then p 'U' q in ({(A => TFALSUM)} \/ (tau1 . A)) \/ (tau1 . TFALSUM) by Def4;
then A2: ( p 'U' q in {(A => TFALSUM)} \/ (tau1 . A) or p 'U' q in tau1 . TFALSUM ) by XBOOLE_0:def 3;
p 'U' q <> TFALSUM by HILBERT2:23;
then not p 'U' q in {TFALSUM} by TARSKI:def 1;
then ( p 'U' q in {(A => TFALSUM)} or p 'U' q in tau1 . A ) by A2, Def4, XBOOLE_0:def 3;
hence p 'U' q in tau1 . A by A1, TARSKI:def 1; :: thesis: verum