let p, q be Element of LTLB_WFF ; :: thesis: tau1 . q c= tau1 . (p 'or' q)
set pq = p 'or' q;
set np = 'not' p;
set nq = 'not' q;
set npq = ('not' p) '&&' ('not' q);
( tau1 . ('not' q) c= tau1 . (('not' p) '&&' ('not' q)) & tau1 . q c= tau1 . ('not' q) ) by Th13, Th12;
then A1: tau1 . q c= tau1 . (('not' p) '&&' ('not' q)) ;
tau1 . (('not' p) '&&' ('not' q)) c= tau1 . (p 'or' q) by Th12;
hence tau1 . q c= tau1 . (p 'or' q) by A1; :: thesis: verum