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

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