let A be Element of LTLB_WFF ; ('not' (TVERUM '&&' ('not' A))) => A is ctaut
let g be Function of LTLB_WFF,BOOLEAN; LTLAXIO1:def 16 (VAL g) . (('not' (TVERUM '&&' ('not' A))) => A) = 1
set v = VAL g;
set t = TVERUM ;
A1:
(VAL g) . TFALSUM = 0
by LTLAXIO1:def 15;
A2:
( (VAL g) . A = 0 or (VAL g) . A = 1 )
by XBOOLEAN:def 3;
thus (VAL g) . (('not' (TVERUM '&&' ('not' A))) => A) =
((VAL g) . ('not' (TVERUM '&&' ('not' A)))) => ((VAL g) . A)
by LTLAXIO1:def 15
.=
(((VAL g) . (TVERUM '&&' ('not' A))) => ((VAL g) . TFALSUM)) => ((VAL g) . A)
by LTLAXIO1:def 15
.=
((((VAL g) . TVERUM) '&' ((VAL g) . ('not' A))) => ((VAL g) . TFALSUM)) => ((VAL g) . A)
by LTLAXIO1:31
.=
((((VAL g) . TVERUM) '&' (((VAL g) . A) => ((VAL g) . TFALSUM))) => ((VAL g) . TFALSUM)) => ((VAL g) . A)
by LTLAXIO1:def 15
.=
1
by A2, A1, Th4
; verum