let A, B, p, q be Element of LTLB_WFF ; :: thesis: ( not p 'U' q in tau1 . (A '&&' B) or p 'U' q in tau1 . A or p 'U' q in tau1 . B )
set a = p 'U' q;
set nb = 'not' B;
assume p 'U' q in tau1 . (A '&&' B) ; :: thesis: ( p 'U' q in tau1 . A or p 'U' q in tau1 . B )
then p 'U' q in tau1 . (A => ('not' B)) by Th9;
then p 'U' q in ({(A => ('not' B))} \/ (tau1 . A)) \/ (tau1 . ('not' B)) by Def4;
then A1: p 'U' q in {(A => ('not' B))} \/ ((tau1 . A) \/ (tau1 . ('not' B))) by XBOOLE_1:4;
p 'U' q <> A => ('not' B) by HILBERT2:22;
then not p 'U' q in {(A => ('not' B))} by TARSKI:def 1;
then p 'U' q in (tau1 . A) \/ (tau1 . ('not' B)) by A1, XBOOLE_0:def 3;
then ( p 'U' q in tau1 . A or p 'U' q in tau1 . ('not' B) ) by XBOOLE_0:def 3;
hence ( p 'U' q in tau1 . A or p 'U' q in tau1 . B ) by Th9; :: thesis: verum