:: deftheorem defines exhaustive POLNOT_1:def 29 :
for X, Y being set
for F being PartFunc of X,(bool Y) holds
( F is exhaustive iff for a being object st a in Y holds
ex b being object st
( b in dom F & a in F . b ) );