let S be non empty finite set ; for BS being Subset of S ex judgefunc being Function of S,BOOLEAN st Coim (judgefunc,TRUE) = BS
let BS be Subset of S; ex judgefunc being Function of S,BOOLEAN st Coim (judgefunc,TRUE) = BS
reconsider f = chi (BS,S) as Function of S,BOOLEAN by MARGREL1:def 11;
A1:
dom f = S
by FUNCT_2:def 1;
A2:
for x being object holds
( x in BS iff x in Coim (f,TRUE) )
take
f
; Coim (f,TRUE) = BS
thus
Coim (f,TRUE) = BS
by A2, TARSKI:2; verum