:: deftheorem defines |= PL_AXIOM:def 17 :
for F being Subset of PL-WFF
for p being Element of PL-WFF holds
( F |= p iff for M being PLModel st M |= F holds
M |= p );