theorem Th18: :: DIST_2:18

for S being non empty finite set
for s being Element of S *
for judgefunc being Function of S,BOOLEAN holds Coim ((judgefunc * s),TRUE) in bool (dom s)