:: deftheorem Def5 defines tau LTLAXIO3:def 5 :
for X, b₂ being Subset of LTLB_WFF holds
( b₂ = tau X iff for x being set holds
( x in b₂ iff ex A being Element of LTLB_WFF st
( A in X & x in tau1 . A ) ) );