:: deftheorem defines -covering FOMODEL2:def 40 :
for S being Language
for X being set holds
( X is S -covering iff for phi being wff string of S holds
( phi in X or xnot phi in X ) );