theorem Th15: :: LTLAXIO4:15

for F being non empty finite Subset of LTLB_WFF ex p being Element of LTLB_WFF st
( p in tau F & tau ((tau F) \ {p}) = (tau F) \ {p} )