:: deftheorem defines LTL_TAUT_OF_PL LTLAXIO1:def 16 :
for p being Element of LTLB_WFF holds
( p is LTL_TAUT_OF_PL iff for f being Function of LTLB_WFF,BOOLEAN holds (VAL f) . p = 1 );