let p, q be Element of LTLB_WFF ; :: thesis: tau1 . q c= tau1 . (p '&&' q)
set pq = p '&&' q;
set np = 'not' p;
set nq = 'not' q;
A1: tau1 . (p => ('not' q)) c= tau1 . ('not' (p => ('not' q))) by Th12;
tau1 . (p => ('not' q)) = ({(p => ('not' q))} \/ (tau1 . p)) \/ (tau1 . ('not' q)) by Def4;
then A2: tau1 . ('not' q) c= tau1 . (p => ('not' q)) by XBOOLE_1:7;
tau1 . q c= tau1 . ('not' q) by Th12;
then tau1 . q c= tau1 . (p => ('not' q)) by A2;
hence tau1 . q c= tau1 . (p '&&' q) by A1; :: thesis: verum