:: deftheorem defines Subt LTLAXIO3:def 7 :
for X being Subset of LTLB_WFF holds Subt X = { (Sub . A) where A is Element of LTLB_WFF : A in X } ;