theorem Th11: :: DILWORTH:11

for R being transitive RelStr
for C being Clique of R
for x, y being Element of R st x is_maximal_in C & x <= y holds
C \/ {y} is Clique of R