theorem inder: :: PL_AXIOM:69

for F being Subset of PL-WFF st F is maximal & F is consistent holds
for p being Element of PL-WFF holds
( F |- p iff p in F )