:: deftheorem Def6 defines Sub LTLAXIO3:def 6 :
for b₁ being Function of LTLB_WFF,(bool LTLB_WFF) holds
( b₁ = Sub iff for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b₁ . TFALSUM = {TFALSUM} & b₁ . (prop n) = {(prop n)} & b₁ . (A => B) = ({(A => B)} \/ (b₁ . A)) \/ (b₁ . B) & b₁ . (A 'U' B) = ((tau1 . (untn (A,B))) \/ (b₁ . A)) \/ (b₁ . B) ) );