:: deftheorem Def18 defines LTL_axioms LTLAXIO1:def 18 :
for b₁ being Subset of LTLB_WFF holds
( b₁ = LTL_axioms iff ( b₁ is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
b₁ c= D ) ) );