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 A1: 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
A2: f is bijective and
A3: for x being set st x in A holds
x in f . x by A1, Th47;
let c be set ; :: thesis: ( c in C implies ex a being Element of A st c /\ A = {a} )
assume A4: c in C ; :: thesis: ex a being Element of A st c /\ A = {a}
rng f = C by A2, FUNCT_2:def 3;
then consider x being object such that
A5: x in dom f and
A6: c = f . x by A4, FUNCT_1:def 3;
A7: x in c by A5, A6, A3;
reconsider a = x as Element of A by A5;
take a ; :: thesis: c /\ A = {a}
now :: thesis: for z being object holds
( ( z in c /\ A implies z = a ) & ( z = a implies z in c /\ A ) )
let z be object ; :: 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 A8: ( z in c & z in A ) by XBOOLE_0:def 4;
c is Clique of R by A4, Def11;
hence z = a by A8, A7, Th15; :: thesis: verum
end;
assume z = a ; :: thesis: z in c /\ A
hence z in c /\ A by A7, A5, XBOOLE_0:def 4; :: thesis: verum
end;
hence c /\ A = {a} by TARSKI:def 1; :: thesis: verum