theorem mon: :: LTLAXIO5:46

for A being Element of LTLB_WFF
for F, G being Subset of LTLB_WFF st F c= G & F |-0 A holds
G |-0 A