theorem Th59: :: POLNOT_1:59

for X, Y being set
for F being PartFunc of X,(bool Y) holds
( not F is exhaustive iff ex a being object st
( a in Y & ( for b being object st b in dom F holds
not a in F . b ) ) ) ;