theorem ct: :: PL_AXIOM:70

for A being Element of PL-WFF
for F being Subset of PL-WFF st F |= A holds
F |- A