theorem Th34: :: DILWORTH:34

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