let p be Element of LTLB_WFF ; :: thesis: p => ('not' ('not' p)) is ctaut
let g be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL g) . (p => ('not' ('not' p))) = 1
set v = VAL g;
A1: (VAL g) . TFALSUM = 0 by LTLAXIO1:def 15;
A2: ( (VAL g) . p = 1 or (VAL g) . p = 0 ) by XBOOLEAN:def 3;
thus (VAL g) . (p => ('not' ('not' p))) = ((VAL g) . p) => ((VAL g) . ('not' ('not' p))) by LTLAXIO1:def 15
.= ((VAL g) . p) => (((VAL g) . ('not' p)) => ((VAL g) . TFALSUM)) by LTLAXIO1:def 15
.= ((VAL g) . p) => ((((VAL g) . p) => ((VAL g) . TFALSUM)) => ((VAL g) . TFALSUM)) by LTLAXIO1:def 15
.= 1 by A2, A1 ; :: thesis: verum