let p be Element of LTLB_WFF ; :: thesis: tau1 . p c= tau1 . ('not' p)
set np = 'not' p;
set f = TFALSUM ;
A1: tau1 . p c= {('not' p)} \/ (tau1 . p) by XBOOLE_1:7;
( {('not' p)} \/ (tau1 . p) c= ({('not' p)} \/ (tau1 . p)) \/ (tau1 . TFALSUM) & tau1 . ('not' p) = ({('not' p)} \/ (tau1 . p)) \/ (tau1 . TFALSUM) ) by XBOOLE_1:7, Def4;
hence tau1 . p c= tau1 . ('not' p) by A1; :: thesis: verum