let R be finite RelStr ; :: thesis: for A being StableSet of R
for C being Clique-partition of R st card C = card A holds
for c being set st c in C holds
ex a being Element of A st c /\ A = {a}
let A be StableSet of R; :: thesis: for C being Clique-partition of R st card C = card A holds
for c being set st c in C holds
ex a being Element of A st c /\ A = {a}
let C be Clique-partition of R; :: thesis: ( card C = card A implies for c being set st c in C holds
ex a being Element of A st c /\ A = {a} )
assume A: card C = card A ; :: thesis: for c being set st c in C holds
ex a being Element of A st c /\ A = {a}
consider f being Function of A,C such that
B: f is bijective and
C: for x being set st x in A holds
x in f . x by A, ACpart1;
let c be set ; :: thesis: ( c in C implies ex a being Element of A st c /\ A = {a} )
assume D: c in C ; :: thesis: ex a being Element of A st c /\ A = {a}
rng f = C by B, FUNCT_2:def 3;
then consider x being set such that
E: x in dom f and
F: c = f . x by D, FUNCT_1:def 5;
G: x in c by E, F, C;
reconsider a = x as Element of A by E;
take a ; :: thesis: c /\ A = {a}

now

let z be set ; :: thesis: ( ( z in c /\ A implies z = a ) & ( z = a implies z in c /\ A ) )

hereby :: thesis: ( z = a implies z in c /\ A )

assume z in c /\ A ; :: thesis: z = a
then A1: ( z in c & z in A ) by XBOOLE_0:def 4;
c is Clique of R by D, LCpart;
hence z = a by A1, G, ACClique; :: thesis: verum

end;

assume z = a ; :: thesis: z in c /\ A
hence z in c /\ A by G, E, XBOOLE_0:def 4; :: thesis: verum

end;

hence c /\ A = {a} by TARSKI:def 1; :: thesis: verum