theorem Th31: :: LTLAXIO1:31

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