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