let R be RelStr ; :: thesis: for C being Clique of R
for A being StableSet of R
for a, b being set st a in A & b in A & a in C & b in C holds
a = b
let C be Clique of R; :: thesis: for A being StableSet of R
for a, b being set st a in A & b in A & a in C & b in C holds
a = b
let A be StableSet of R; :: thesis: for a, b being set st a in A & b in A & a in C & b in C holds
a = b
let a, b be set ; :: thesis: ( a in A & b in A & a in C & b in C implies a = b )
assume that
A1: ( a in A & b in A ) and
A2: ( a in C & b in C ) ; :: thesis: a = b
assume A3: a <> b ; :: thesis: contradiction
reconsider a9 = a, b9 = b as Element of R by A1;
( not a9 <= b9 & not b9 <= a9 ) by A1, A3, Def2;
hence contradiction by A2, A3, Th6; :: thesis: verum