let p, q be Element of LTLB_WFF ; :: thesis: for g being Function of LTLB_WFF,BOOLEAN holds (VAL g) . (p 'or' q) = ((VAL g) . p) 'or' ((VAL g) . q)
let g be Function of LTLB_WFF,BOOLEAN; :: thesis: (VAL g) . (p 'or' q) = ((VAL g) . p) 'or' ((VAL g) . q)
set v = VAL g;
A1: (VAL g) . TFALSUM = FALSE by LTLAXIO1:def 15;
thus (VAL g) . (p 'or' q) = ((VAL g) . (('not' p) '&&' ('not' q))) => ((VAL g) . TFALSUM) by LTLAXIO1:def 15
.= (((VAL g) . ('not' p)) '&' ((VAL g) . ('not' q))) => ((VAL g) . TFALSUM) by LTLAXIO1:31
.= ((((VAL g) . p) => ((VAL g) . TFALSUM)) '&' ((VAL g) . ('not' q))) => ((VAL g) . TFALSUM) by LTLAXIO1:def 15
.= ((((VAL g) . p) => ((VAL g) . TFALSUM)) '&' (((VAL g) . q) => ((VAL g) . TFALSUM))) => ((VAL g) . TFALSUM) by LTLAXIO1:def 15
.= ((VAL g) . p) 'or' ((VAL g) . q) by A1 ; :: thesis: verum