let A, B be Element of LTLB_WFF ; :: thesis: 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; :: thesis: 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; :: thesis: verum