let p, q be Element of LTLB_WFF ; :: thesis: for X being Subset of LTLB_WFF holds X |- ('X' (p 'or' q)) => (('X' p) 'or' ('X' q))
let X be Subset of LTLB_WFF; :: thesis: X |- ('X' (p 'or' q)) => (('X' p) 'or' ('X' q))
set xp = 'X' p;
set xq = 'X' q;
set np = 'not' p;
set nq = 'not' q;
set xnp = 'X' ('not' p);
set xnq = 'X' ('not' q);
set nxp = 'not' ('X' p);
set nxq = 'not' ('X' q);
X |- (('X' ('not' p)) '&&' ('X' ('not' q))) => ('X' (('not' p) '&&' ('not' q))) by LTLAXIO1:53;
then A1: X |- ('not' ('X' (('not' p) '&&' ('not' q)))) => ('not' (('X' ('not' p)) '&&' ('X' ('not' q)))) by LTLAXIO1:52;
('not' ('X' q)) => ('X' ('not' q)) in LTL_axioms by LTLAXIO1:def 17;
then A2: X |- ('not' ('X' q)) => ('X' ('not' q)) by LTLAXIO1:42;
('not' ('X' p)) => ('X' ('not' p)) in LTL_axioms by LTLAXIO1:def 17;
then X |- ('not' ('X' p)) => ('X' ('not' p)) by LTLAXIO1:42;
then X |- (('not' ('X' p)) '&&' ('not' ('X' q))) => (('X' ('not' p)) '&&' ('X' ('not' q))) by A2, Th53;
then A3: X |- ('not' (('X' ('not' p)) '&&' ('X' ('not' q)))) => ('not' (('not' ('X' p)) '&&' ('not' ('X' q)))) by LTLAXIO1:52;
('X' (p 'or' q)) => ('not' ('X' (('not' p) '&&' ('not' q)))) in LTL_axioms by LTLAXIO1:def 17;
then X |- ('X' (p 'or' q)) => ('not' ('X' (('not' p) '&&' ('not' q)))) by LTLAXIO1:42;
then X |- ('X' (p 'or' q)) => ('not' (('X' ('not' p)) '&&' ('X' ('not' q)))) by A1, LTLAXIO1:47;
hence X |- ('X' (p 'or' q)) => (('X' p) 'or' ('X' q)) by A3, LTLAXIO1:47; :: thesis: verum