let S be non empty finite set ; :: thesis: for BS being Subset of S ex judgefunc being Function of S,BOOLEAN st Coim (judgefunc,TRUE) = BS
let BS be Subset of S; :: thesis: 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) )

proof

let x be object ; :: thesis: ( x in BS iff x in Coim (f,TRUE) )
A3: ( x in BS implies f . x in {TRUE} )

proof

assume A4: x in BS ; :: thesis: f . x in {TRUE}
f . x = TRUE by A4, FUNCT_3:def 3;
hence f . x in {TRUE} by TARSKI:def 1; :: thesis: verum

end;

( f . x in {TRUE} implies x in BS )

proof

assume f . x in {TRUE} ; :: thesis: x in BS
then f . x = TRUE by TARSKI:def 1;
hence x in BS by FUNCT_3:36; :: thesis: verum

end;

hence ( x in BS iff x in Coim (f,TRUE) ) by A3, A1, FUNCT_1:def 7; :: thesis: verum

end;

take f ; :: thesis: Coim (f,TRUE) = BS
thus Coim (f,TRUE) = BS by A2, TARSKI:2; :: thesis: verum