theorem Th5: :: LTLAXIO2:5

for p, q being Element of LTLB_WFF
for g being Function of LTLB_WFF,BOOLEAN holds (VAL g) . (p 'or' q) = ((VAL g) . p) 'or' ((VAL g) . q)