let Y be non empty set ; :: thesis:
let a be Function of Y,BOOLEAN; :: thesis:
for F being set st F in %I Y holds
for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2

let F be set ; :: thesis:
assume F in %I Y ; :: thesis:
then F in { B where B is Subset of Y : ex z being set st
( B = {z} & z in Y ) } by PARTIT1:31;
then ex B being Subset of Y st
( F = B & ex z being set st
( B = {z} & z in Y ) ) ;
then consider z being set such that
A1: F = {z} and
z in Y ;
let x1, x2 be set ; :: thesis:
assume that
A2: x1 in F and
A3: x2 in F ; :: thesis:
x1 = z by A1, A2, TARSKI:def 1;
hence a . x1 = a . x2 by A1, A3, TARSKI:def 1; :: thesis:

end;