let g be Function of LTLB_WFF,BOOLEAN; :: thesis: (VAL g) . TVERUM = 1
thus (VAL g) . TVERUM = ((VAL g) . TFALSUM) => ((VAL g) . TFALSUM) by LTLAXIO1:def 15
.= FALSE => ((VAL g) . TFALSUM) by LTLAXIO1:def 15
.= 1 ; :: thesis: verum