theorem Th14: :: LTLAXIO4:14

for Q being PNPair
for X being non empty Subset of [:(LTLB_WFF **),(LTLB_WFF **):] st Q in X holds
comp Q c= comp X