theorem Th35: :: DILWORTH:35

for R being transitive RelStr
for A being StableSet of R
for C being Clique of (subrelstr (Upper A))
for a, b being Element of R st a in A & a in C & b in C & not a = b holds
a <= b