theorem Th25: :: LTLAXIO3:25

for p being Element of LTLB_WFF holds tau1 . p c= Sub . p