theorem Th12: :: DILWORTH:12

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