let A, B be Element of LTLB_WFF ; for X being Subset of LTLB_WFF holds X |- ('not' (A 'U' B)) => ('X' ('not' (untn (A,B))))
let X be Subset of LTLB_WFF; X |- ('not' (A 'U' B)) => ('X' ('not' (untn (A,B))))
set p = A 'U' B;
set q = 'X' B;
set r = 'X' (A '&&' (A 'U' B));
(('X' B) 'or' ('X' (A '&&' (A 'U' B)))) => (A 'U' B) in LTL_axioms
by LTLAXIO1:def 17;
then A1:
X |- (('X' B) 'or' ('X' (A '&&' (A 'U' B)))) => (A 'U' B)
by LTLAXIO1:42;
X |- ('X' (untn (A,B))) => (('X' B) 'or' ('X' (A '&&' (A 'U' B))))
by Th62;
then
X |- ('X' (untn (A,B))) => (A 'U' B)
by LTLAXIO1:47, A1;
then A2:
X |- ('not' (A 'U' B)) => ('not' ('X' (untn (A,B))))
by LTLAXIO1:52;
('not' ('X' (untn (A,B)))) => ('X' ('not' (untn (A,B)))) in LTL_axioms
by LTLAXIO1:def 17;
then
X |- ('not' ('X' (untn (A,B)))) => ('X' ('not' (untn (A,B))))
by LTLAXIO1:42;
hence
X |- ('not' (A 'U' B)) => ('X' ('not' (untn (A,B))))
by LTLAXIO1:47, A2; verum