for A being Element of LTLB_WFF
for P being PNPair st A in rng (P `1) holds
{} LTLB_WFF |- (P ^) => A