:: deftheorem Def15 defines VAL LTLAXIO1:def 15 :
for f, b₂ being Function of LTLB_WFF,BOOLEAN holds
( b₂ = VAL f iff for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b₂ . TFALSUM = 0 & b₂ . (prop n) = f . (prop n) & b₂ . (A => B) = (b₂ . A) => (b₂ . B) & b₂ . (A 'U' B) = f . (A 'U' B) ) );