theorem Th58: :: LTLAXIO2:58

for p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF holds X |- (('X' p) => ('X' q)) => ('X' (p => q))