let p, q be Element of LTLB_WFF ; :: thesis: for X being Subset of LTLB_WFF holds X |- (('X' p) '&&' ('X' q)) => ('X' (p '&&' q))
let X be Subset of LTLB_WFF; :: thesis: X |- (('X' p) '&&' ('X' q)) => ('X' (p '&&' q))
set Xp = 'X' p;
set nq = 'not' q;
set nXq = 'not' ('X' q);
set Xnq = 'X' ('not' q);
('X' ('not' q)) => ('not' ('X' q)) in LTL_axioms by Def17;
then A1: X |- ('X' ('not' q)) => ('not' ('X' q)) by Th42;
('not' ('X' (p => ('not' q)))) => ('X' ('not' (p => ('not' q)))) in LTL_axioms by Def17;
then A2: X |- ('not' ('X' (p => ('not' q)))) => ('X' ('not' (p => ('not' q)))) by Th42;
('X' (p => ('not' q))) => (('X' p) => ('X' ('not' q))) in LTL_axioms by Def17;
then X |- ('X' (p => ('not' q))) => (('X' p) => ('X' ('not' q))) by Th42;
then X |- ('X' (p => ('not' q))) => (('X' p) => ('not' ('X' q))) by A1, Th51;
then X |- ('not' (('X' p) => ('not' ('X' q)))) => ('not' ('X' (p => ('not' q)))) by Th52;
hence X |- (('X' p) '&&' ('X' q)) => ('X' (p '&&' q)) by A2, Th47; :: thesis: verum