theorem mon2: :: LTLAXIO5:2
for A being Element of LTLB_WFF
for F, G being Subset of LTLB_WFF st F c= G & F |- A holds
G |- A